/*
 * All of the documentation and software included in the
 * Alchemy Software is copyrighted by Stanley Kok, Parag
 * Singla, Matthew Richardson, Pedro Domingos, Marc
 * Sumner, Hoifung Poon, Daniel Lowd, and Jue Wang.
 *
 * Copyright [2004-09] Stanley Kok, Parag Singla, Matthew
 * Richardson, Pedro Domingos, Marc Sumner, Hoifung
 * Poon, Daniel Lowd, and Jue Wang. All rights reserved.
 *
 * Contact: Pedro Domingos, University of Washington
 * (pedrod@cs.washington.edu).
 *
 * Redistribution and use in source and binary forms, with
 * or without modification, are permitted provided that
 * the following conditions are met:
 *
 * 1. Redistributions of source code must retain the above
 * copyright notice, this list of conditions and the
 * following disclaimer.
 *
 * 2. Redistributions in binary form must reproduce the
 * above copyright notice, this list of conditions and the
 * following disclaimer in the documentation and/or other
 * materials provided with the distribution.
 *
 * 3. All advertising materials mentioning features or use
 * of this software must display the following
 * acknowledgment: "This product includes software
 * developed by Stanley Kok, Parag Singla, Matthew
 * Richardson, Pedro Domingos, Marc Sumner, Hoifung
 * Poon, Daniel Lowd, and Jue Wang in the Department of
 * Computer Science and Engineering at the University of
 * Washington".
 *
 * 4. Your publications acknowledge the use or
 * contribution made by the Software to your research
 * using the following citation(s):
 * Stanley Kok, Parag Singla, Matthew Richardson and
 * Pedro Domingos (2005). "The Alchemy System for
 * Statistical Relational AI", Technical Report,
 * Department of Computer Science and Engineering,
 * University of Washington, Seattle, WA.
 * http://alchemy.cs.washington.edu.
 *
 * 5. Neither the name of the University of Washington nor
 * the names of its contributors may be used to endorse or
 * promote products derived from this software without
 * specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE UNIVERSITY OF WASHINGTON
 * AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED
 * WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
 * PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE UNIVERSITY
 * OF WASHINGTON OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT,
 * INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
 * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
 * ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
 * IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 */
#ifndef FOLHELPER_H_JUL_21_2005
#define FOLHELPER_H_JUN_21_2005

// dl library used for dynamically loading linked-in functions
#include <dlfcn.h>
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <signal.h>
#include <ext/hash_set>
#include <stack>
#include <iostream>
#include <fstream>
#include <sstream>
#include "strfifolist.h"
#include "predicate.h"
#include "function.h"
#include "clause.h"
#include "clausefactory.h"
#include "hashstring.h"
#include "database.h"
#include "listobj.h"
#include "timer.h"
#include "internals.h"

//NOTE: When a variable is added, please init it in zzinit() and destroy it
//      in zzcleanUp(). Add it in zzreset() if it has to be reinitialized before
//      a new clause is parsed.


  //Each hard clause derived from a hard formula is given a weight that is twice
  //that of the maximum soft clause weight. You can change this value by setting
  //HARD_WEIGHT_MULTIPLIER below. If you wish to set the hard clause weight to
  //a specific value, you can set HARD_WEIGHT below.
  //If HARD_WEIGHT is DBL_MIN, HARD_WEIGHT_MULTIPLIER is used instead of
  //HARD_WEIGHT; otherwise the latter is used.
//const double HARD_WEIGHT_MULTIPLIER = 200000;
//const double HARD_WEIGHT = DBL_MIN;
const double HARD_WEIGHT_MULTIPLIER = 10;
const double HARD_WEIGHT = 10;

  // If the variables are assigned some initial values, ensure they are are
  // similarly assigned in zzinit(). Also set any data structure to its initial
  // state in zzinit()
const int ZZ_MAX_ERRORS = 50;

// Start of variable names generated by replacement of functions
const char* ZZ_FUNCVAR_PREFIX = "funcVar";

// Name of shared object file for linked-in functions
const char* ZZ_FUNCTION_SO_FILE = "functions.so";

  // a copy of the user-specified MLN file is created & appended with this str
const char* ZZ_TMP_FILE_POSTFIX = "_tmpalchemy.mln";

  // prepend to a file containing query predicates
const char* zzdefaultPredName = "SKPRED";
const char* zzdefaultFuncName = "SKFUNC";
const char* zzdefaultTypeName = "SKTYPE";
const char* zzdefaultVarName  = "SKVAR";

bool zzstoreGroundPreds = false; //set to true for testing only
  //constants must be declared before being used
bool zzconstantMustBeDeclared = false;
  // read weight that is specified for a hard formula
bool zzreadHardClauseWts = false;
  //used in follex.y to allow predicate definitions to be on the same line
bool zzafterRtParen;

bool zzisParsing; //indicates whether a file is currently being parsed
double zzdefaultWt; // default wt of a formula if no wt or . is specified
  //a formula must begin with a weight or end with full stop
bool zzmustHaveWtOrFullStop;
  // indicates whether weights should be flipped when a clause is flipped.
  // This should be true for inference and false for learning.
bool zzflipWtsOfFlippedClause;
bool zzwarnDuplicates;
string zzinFileName;
char zzerrMsg[1024];

int zzcount;  // to be appended to names of default pred, type etc.
int zzline, zzcolumn;
int zznumCharRead;
int zznumErrors;
bool zzok;
MLN* zzmln;
Domain* zzdomain;
int zznumEofSeen; // num of times EOF seen
StrFifoList zztokenList;

char* zztypeName;
PredicateTemplate* zzpredTemplate;
FunctionTemplate* zzfuncTemplate;
Predicate* zzpred;
Function* zzfunc;
stack<Function*> zzfuncStack;
stack<ListObj*> zzfuncConjStack;
double* zzwt;
double* zzutil;
double* zzrealValue;
bool zzisNegated;
bool zzisAsterisk;
bool zzisPlus;
bool zzhasFullStop;
bool zzhasWeightFullStop;
bool zzinIndivisible;
bool zzisHybrid;
int zznumAsterisk;
char zztrueFalseUnknown;
string zzformulaStr;
string zzfuncConjStr;
bool zzparseGroundPred;
stack<ListObj*> zzformulaListObjs;  //used by formulas with connectives
stack<ListObj*> zzpredFuncListObjs; // used by predicates and functions
hash_map<int, PredicateHashArray*> zzpredIdToGndPredMap;
ListObj* zzcontPred;
double zzmean;

// Used to check if there is a function definition
int zzfdnumPreds;
int zzfdnumFuncs;
int zzfdnumVars;
int zzfuncVarCounter = 0;
//bool zzfdisEqualPred;
string zzfdfuncName;
Array<string> zzfdfuncConstants;
string zzfdconstName;
// Used in function definitions to store the return value and type
char* zztmpReturnConstant;
bool zztmpReturnNum;

// Used to store first number in numeric declarations
int zzinitialNumDeclaration;

// Set to true if using linked-in predicates
bool zzusingLinkedPredicates;
// Set to true if using linked-in functions
bool zzusingLinkedFunctions;

// Needed to hold list object information while function is replaced
ListObj* zzoldFuncLo;
Timer zztimer;

// Holds the internally implemented predicates and their types (see zzinit())
Array<Array<const char*> > zzinternalPredicates;
// Holds the internally implemented functions and their types (see zzinit())
Array<Array<const char*> > zzinternalFunctions;

// If an infix predicate is encountered then the name of it is stored here
char* zzinfixPredName;
// If an infix function is encountered then the name of it is stored here
char* zzinfixFuncName;

///////// store '=' preds for which the types on both sides are unknown //////
struct ZZUnknownEqPredInfo
{
  ZZUnknownEqPredInfo(const string& name, const string& lhs, const string& rhs)
    :name_(name), lhs_(lhs), rhs_(rhs) {}

  string name_; //e.g. SK_EQUAL_1
    // variable name on left and right hand side
  string lhs_;
  string rhs_;
};

///// store internal preds for which the types on both sides are unknown //////
struct ZZUnknownIntPredInfo
{
  ZZUnknownIntPredInfo(const string& name, const string& lhs, const string& rhs)
    :name_(name), lhs_(lhs), rhs_(rhs) {}

  string name_; //e.g. greaterThan_1
    // variable name on left and right hand side
  string lhs_;
  string rhs_;
};

/////// store internal funcs for which at least one term type is unknown //////
struct ZZUnknownIntFuncInfo
{
  ZZUnknownIntFuncInfo(const string& name, const Array<string>& vnames)
    :name_(name), vnames_(vnames) {}

  string name_; //e.g. plus_1
    // variable names
  Array<string> vnames_;
};

  // counts the number of '=' predicates for which both LHS and RHS are unknown
int zzeqTypeCounter;
  // counts the number of internal predicates for which both LHS and RHS are
  // unknown
int zzintPredTypeCounter;
  // counts the number of internal functions for which at least one term type is
  // unknown
int zzintFuncTypeCounter;

  // list of '=' predicates for which both LHS and RHS are unknown
list<ZZUnknownEqPredInfo> zzeqPredList;
  // list of internal predicates for which both LHS and RHS are unknown
list<ZZUnknownIntPredInfo> zzintPredList;
  // list of internal functions for which at least one term type is unknown
list<ZZUnknownIntFuncInfo> zzintFuncList;


/////////// store state necessary to support "#include" statement //////////

struct ZZFileState
{
  ZZFileState(FILE* const & file, const string& inFileName,
              const int& numCharRead, const int& line, const int& column)
    : file_(file), inFileName_(inFileName), numCharRead_(numCharRead),
      line_(line), column_(column) {}

  FILE* file_;
  string inFileName_;
  int numCharRead_;
  int line_;
  int column_;
};

stack<ZZFileState> zzinStack;

///////////// ensure variable name, id, and type consistency ////////////////

int zzvarCounter;
int zzanyTypeId;

struct ZZVarIdType
{
  ZZVarIdType() : id_(0), typeId_(0) {}

  ZZVarIdType(const ZZVarIdType& varIdType)
    : id_(varIdType.id_), typeId_(varIdType.typeId_) {}

  ZZVarIdType(const int& varId, const int& typeId)
    : id_(varId), typeId_(typeId) {}

  int id_;
  int typeId_;
};


  // contains variables names
typedef hash_map<const string, ZZVarIdType, HashString, EqualString>
  ZZVarNameToIdMap;

ZZVarNameToIdMap zzvarNameToIdMap;

  // contains mappings of functions to funcVars which replace them
typedef hash_map<Function*, string, HashFunction, EqualFunction>
  ZZFuncToFuncVarMap;

ZZFuncToFuncVarMap zzfuncToFuncVarMap;


  // maps a variable name to a new one that has its scope number appended
typedef hash_map<string, string, HashString, EqualString> StringToStringMap;

int zzscopeCounter; // identifies a scope

  // using a list so that we can iterate through the elements in the stack
  // the front and back correspond to the the top and bottom of a stack
typedef list< pair<StringToStringMap*,int> > ZZOldNewVarList;
ZZOldNewVarList zzoldNewVarList;


  // since plus variables e.g. x in P(+x,y) cannot be explicitly
  // universally/existentially quantified, they must exist within the scope of
  // the entire formula
typedef hash_map<string, int, HashString, EqualString> StringToIntMap;
StringToIntMap zzplusVarMap;


////////// store the information about a formula for later processsing ////////
struct ZZFormulaInfo
{
  ZZFormulaInfo(const ListObj* const & fformula, const string& fformulaStr,
                const int& nnumPreds, const double* const & wwt,
                const double& ddefaultWt, const Domain* const& ddomain,
                MLN* const & mmln, const ZZVarNameToIdMap& vvarNameToIdMap,
                const StringToIntMap& pplusVarMap, const int& nnumAsterisk,
                const bool& hhasFullStop,
                const bool& rreadHardClauseWts,
                const bool& mmustHaveWtOrFullStop,
                const bool& iisIndivisible, const bool& iisHybrid,
                const ListObj* const & ccontPred, const double& mmean,
                const bool& hhasWeightFullStop, const double* const & uutil)
    : formula(fformula), formulaStr(fformulaStr), numPreds(nnumPreds),
      defaultWt(ddefaultWt), domain(ddomain), mln(mmln),
      numAsterisk(nnumAsterisk), hasFullStop(hhasFullStop),
      readHardClauseWts(rreadHardClauseWts),
      mustHaveWtOrFullStop(mmustHaveWtOrFullStop),
      isIndivisible(iisIndivisible), isHybrid(iisHybrid),
      contPred(ccontPred), mean(mmean), hasWeightFullStop(hhasWeightFullStop)
  {
    wt = (wwt) ? new double(*wwt) : NULL;
    util = (uutil) ? new double(*uutil) : NULL;

    ZZVarNameToIdMap::const_iterator it = vvarNameToIdMap.begin();
    for (; it != vvarNameToIdMap.end(); it++)
      varNameToIdMap[(*it).first] = ZZVarIdType((*it).second);

    StringToIntMap::const_iterator itt = pplusVarMap.begin();
    for (; itt != pplusVarMap.end(); itt++)
      plusVarMap[(*itt).first] = (*itt).second;
  }

  ~ZZFormulaInfo() { if (wt) delete wt; if (util) delete util; }

  const ListObj* formula;
  const string formulaStr;
  const int numPreds;
  const double* wt;
  const double defaultWt;
  const Domain* domain;
  MLN* mln;
  ZZVarNameToIdMap varNameToIdMap;
  StringToIntMap plusVarMap;
  const int numAsterisk;
  const bool hasFullStop;
  const bool readHardClauseWts;
  const bool mustHaveWtOrFullStop;
  const bool isIndivisible;
  const bool isHybrid;
  const ListObj* contPred;
  const double mean;
  const bool hasWeightFullStop;
  const double* util;
};

Array<ZZFormulaInfo*> zzformulaInfos;


///////////////////////////////////////////////////////////////////////

string rmTmpPostfix(const string& filename)
{
  unsigned int postfixLen = strlen(ZZ_TMP_FILE_POSTFIX);
  if (filename.length() < postfixLen) return filename;
  if (filename.compare(filename.length() - postfixLen, postfixLen,
                       ZZ_TMP_FILE_POSTFIX, postfixLen)==0)
    return filename.substr(0, filename.length() - postfixLen);
  else
    return filename;
}


void yyerror(char const * err)
{
  string errStr = err;
  if (strncmp(err,"parse error, unexpected '(', expecting '='",42)==0)
    errStr.append("Have you declared the predicate/function preceding '('");

  if (zzisParsing)
    printf("ERROR in %s: line %d, col %d: %s\n",
           rmTmpPostfix(zzinFileName).c_str(),zzline, zzcolumn, errStr.c_str());
  else
    printf("ERROR occurs after parsing %s: %s\n",
           rmTmpPostfix(zzinFileName).c_str(), errStr.c_str());

  zzok=false;
  if (++zznumErrors == ZZ_MAX_ERRORS)
  {
    cout << "Num of errors = " << zznumErrors
         << ". Exceeded maximum number of errors." << endl;
    exit(-1);
  }
}


void zzerr(const char* const & str) { yyerror(str); }


void zzerr(const char* const & str, const char* const & token)
{
  sprintf(zzerrMsg, str, token);
  yyerror(zzerrMsg);
}


void zzerr(const char* const & str, const char* const & token1,
           const char* const & token2)
{
  sprintf(zzerrMsg, str, token1, token2);
  yyerror(zzerrMsg);
}


void zzerr(const char* const & str, const char* const & token1,
           const char* const & token2, const char* const & token3)
{
  sprintf(zzerrMsg, str, token1, token2, token3);
  yyerror(zzerrMsg);
}


void zzerr(const char* const & str, const char* const & token1,
           const int& token2, const int& token3)
{
  sprintf(zzerrMsg, str, token1, token2, token3);
  yyerror(zzerrMsg);
}


void zzwarn(const char* const & str)
{
  if (zzisParsing)
    printf("WARNING in %s: line %d, col %d: %s\n",
           rmTmpPostfix(zzinFileName).c_str(), zzline, zzcolumn, str);
  else
    printf("WARNING after parsing %s: %s\n",
           rmTmpPostfix(zzinFileName).c_str(), str);
}


void zzwarn(const char* const & str, const char* const & token)
{
  sprintf(zzerrMsg, str, token);
  zzwarn(zzerrMsg);
}


void zzexit(const char* const & str)
{
  zzerr(str);
  exit(-1);
}


void zzexit(const char* const & str, const char* const & token)
{
  zzerr(str,token);
  exit(-1);
}


void zzassert(const bool& condn, const char* const & str)
{
  string s("assertion failed! ");
  s.append(str);
  if (!condn) zzexit(s.c_str());
}


void zzmsg(const char* const & str)
{
  if (zzisParsing)
    printf("in %s: line %d, col %d: %s\n",
           rmTmpPostfix(zzinFileName).c_str(), zzline, zzcolumn, str);
  else
    printf("after parsing %s: %s\n", rmTmpPostfix(zzinFileName).c_str(), str);
}


void zzmsg(const char* const & str, const char* const & token)
{
  sprintf(zzerrMsg, str, token);
  zzmsg(zzerrMsg);
}


///////////////////////// manage variable ids ////////////////////////

string zzgetNewVarName(const char* const & varName)
{
  ZZOldNewVarList::iterator it = zzoldNewVarList.begin();
  for (; it != zzoldNewVarList.end(); it++)
  {
    StringToStringMap* oldNewVarMap = (*it).first;
    StringToStringMap::iterator mit;
    if ((mit = oldNewVarMap->find(varName)) != oldNewVarMap->end())
      return (*mit).second;
  }
  return string(varName);
}


  // returns var id (negative number) or 0 if varName is of wrong type
int zzgetVarId(const char* const& varName, const int& varTypeId,
               int& expectedTypeId)
{
  string vname = varName;

    // search last element (which corresponds to the scope of the entire formula
  ZZVarNameToIdMap::iterator mit;
  if ((mit = zzvarNameToIdMap.find(vname)) == zzvarNameToIdMap.end())
  {
    ZZVarIdType v(--zzvarCounter, varTypeId);
    zzvarNameToIdMap[vname] = v;
    return v.id_;
  }

  ZZVarIdType& varIdType = (*mit).second;
  int typeId = varTypeId; //avoid confusion later

  if (varIdType.typeId_ == zzanyTypeId)
  {
    varIdType.typeId_ = typeId;
    expectedTypeId = varIdType.typeId_;
    return varIdType.id_;
  }

//  if (typeId != zzanyTypeId && typeId != varIdType.typeId_)
//  {
//    expectedTypeId = varIdType.typeId_;
//    return 0;
//  }
  return varIdType.id_;
}

int zzgetVarTypeId(const char* const& varName)
{
  ZZVarNameToIdMap::iterator mit;
  if ((mit = zzvarNameToIdMap.find(string(varName))) != zzvarNameToIdMap.end())
    return (*mit).second.typeId_;
  return -1;
}


void zzcheckVarNameToIdMap()
{
  ZZVarNameToIdMap::iterator it = zzvarNameToIdMap.begin();
  for (;it != zzvarNameToIdMap.end(); it++)
    if ((*it).second.typeId_ == zzanyTypeId)
      zzerr("Variable %s has unknown type.", (*it).first.c_str());
}


  // returns var id (negative number) or 0 if varName is of wrong type
bool zzvarIsQuantified(const char* const& varName)
{
  ZZOldNewVarList::iterator it = zzoldNewVarList.begin();
  for (; it != zzoldNewVarList.end(); it++)
  {
    StringToStringMap* oldNewVarMap = (*it).first;
    StringToStringMap::iterator mit;
    if ((mit = oldNewVarMap->find(varName)) != oldNewVarMap->end())
      return true;
  }
  return false;
}


   // Caller must delete the returned VarTypeMap
VarTypeMap* zzcreateVarTypeMap(const ZZVarNameToIdMap& map)
{
  VarTypeMap* vtMap = new VarTypeMap;
  ZZVarNameToIdMap::const_iterator it = map.begin();
  for (; it != map.end(); it++)
    (*vtMap)[(*it).first] =(*it).second.typeId_;
  return vtMap;
}


void zzsetPlusVarTypeId()
{
  StringToIntMap::iterator mit = zzplusVarMap.begin();
  for (; mit != zzplusVarMap.end(); mit++)
  {
    string plusVarName = (*mit).first;
    ZZVarNameToIdMap::iterator typeIt = zzvarNameToIdMap.find(plusVarName);
    zzassert(typeIt != zzvarNameToIdMap.end(),
             "expect typeIt != zzvarNameToIdMap.end()");
    //commented out: done in zzcheckVarNameToIdMap()
    //zzassert((*mit).second.typeId_ > 0,"expect typedId > 0");
    (*mit).second = (*typeIt).second.typeId_;
  }
}


////////////////////////// predicate functions ////////////////////////


/**
 * Checks if the name of a function is that of an internal function.
 *
 * @param funcname Name of function to be checked
 *
 * @return true, if name of function found, otherwise false
 */
bool zzisInternalFunction(const char* funcname)
{
  for (int i = 0; i < zzinternalFunctions.size(); i++)
  	if (strcmp(funcname, zzinternalFunctions[i][0]) == 0)
  	  return true;

  return false;
}

// Returns the index of internal function with name funcname if found,
// otherwise 0
int zzfindInternalFunction(const char* funcname)
{
  for (int i = 0; i < zzinternalFunctions.size(); i++)
    if (strcmp(funcname, zzinternalFunctions[i][0]) == 0)
      return i;
  return -1;
}

/**
 * Checks if the name of a predicate is that of an internal predicate.
 *
 * @param predname Name of predicate to be checked
 *
 * @return true, if name of predicate found, otherwise false
 */
bool zzisInternalPredicate(const char* predname)
{
  for (int i = 0; i < zzinternalPredicates.size(); i++)
  	if (strcmp(predname, zzinternalPredicates[i][0]) == 0)
  	  return true;

  return false;
}

// Returns the index of internal predicate with name predname if found,
// otherwise 0
int zzfindInternalPredicate(const char* predname)
{
  for (int i = 0; i < zzinternalPredicates.size(); i++)
    if (strcmp(predname, zzinternalPredicates[i][0]) == 0)
      return i;
  return -1;
}

/**
 * Checks if the name of a function is that of a linked-in function.
 *
 * @param funcname Name of function to be checked
 * @param handle handle obtained from dlopen() on a file name
 *
 * @return true, if name of function found, otherwise false
 */
bool zzisLinkedFunction(const char* funcname, void* handle)
{
  char *error;

  dlerror();    // Clear any existing error
  dlsym(handle, funcname);
  if ((error = dlerror()) != NULL) return false;

  return true;
}

/**
 * Checks if the name of a predicate is that of a linked-in predicate.
 *
 * @param predname Name of predicate to be checked
 * @param handle handle obtained from dlopen() on a file name
 *
 * @return true, if name of predicate found, otherwise false
 */
bool zzisLinkedPredicate(const char* predname, void* handle)
{
  char *error;

  dlerror();    // Clear any existing error
  dlsym(handle, predname);
  if ((error = dlerror()) != NULL) return false;

  return true;
}

void zzsetEqPredTypeName(const int& typeId)
{
  const char * typeName = zzdomain->getTypeName(typeId);
  string eqPredName = PredicateTemplate::createEqualPredTypeName(typeName);
  const PredicateTemplate* t =
    zzdomain->getPredicateTemplate(eqPredName.c_str());
  zzpred->setTemplate((PredicateTemplate*)t);
  zzassert(t != NULL,
           "expect equal pred template != NULL");
  ListObj* predlo = zzpredFuncListObjs.top();
  predlo->replace(PredicateTemplate::EQUAL_NAME, eqPredName.c_str());
}

int zzgetTypeId(const Term* const & t, const char* const & varName)
{
  int termType = t->getType();
  if (termType == Term::FUNCTION)
    return t->getFunction()->getRetTypeId();

    // Constants could potentially be of any type
  if (termType == Term::CONSTANT)
    return -1;

  if (termType == Term::VARIABLE)
  {
    ZZVarNameToIdMap::iterator mit = zzvarNameToIdMap.find(varName);
    if (mit != zzvarNameToIdMap.end()) return (*mit).second.typeId_;
    return zzanyTypeId;
  }
  zzassert(false, "expect FUNCTION, VARIABLE, CONSTANT");
  return -1;
}


void zzdetermineEqPredTypes(ListObj* const & formula)
{
  unsigned int prevSize = 0;
  while (zzeqPredList.size() != prevSize)
  {
    prevSize = zzeqPredList.size();
    list<ZZUnknownEqPredInfo>::iterator lit, remIt ;
    for (lit = zzeqPredList.begin(); lit != zzeqPredList.end(); lit++)
    {
      ZZUnknownEqPredInfo& uepi = (*lit);
      string lvarName = uepi.lhs_;
      string rvarName = uepi.rhs_;
      int lTypeId = zzgetVarTypeId(lvarName.c_str());
      int rTypeId = zzgetVarTypeId(rvarName.c_str());

      if (lTypeId > 0 && rTypeId > 0) //if both types are known
      {
        if (lTypeId != rTypeId)
          zzerr("The types of %s and %s on the left and right of "
                "'=' must match.", lvarName.c_str(), rvarName.c_str());
        const char * typeName = zzdomain->getTypeName(lTypeId);
        string eqPredName
          = PredicateTemplate::createEqualPredTypeName(typeName);
        formula->replace(uepi.name_.c_str(), eqPredName.c_str());
        remIt = lit; lit++; zzeqPredList.erase(remIt);

      }
      else  // if only one type is known
      if ( (lTypeId<=0 && rTypeId>0) || (lTypeId>0 && rTypeId<=0) )
      {
        int knownTypeId = (lTypeId>0) ? lTypeId : rTypeId;
        const char * typeName = zzdomain->getTypeName(knownTypeId);
        string eqPredName
          = PredicateTemplate::createEqualPredTypeName(typeName);
        formula->replace(uepi.name_.c_str(), eqPredName.c_str());
        const char* unknowVarName = (lTypeId>0) ?  rvarName.c_str() :
                                                   lvarName.c_str();
        zzvarNameToIdMap[unknowVarName].typeId_ = knownTypeId;
        remIt = lit; lit++; zzeqPredList.erase(remIt);
      }
    }
  }
  if (zzeqPredList.size() > 0)
  {
    zzerr("The following variables used with the '=' operator have "
         "unknown types");
    list<ZZUnknownEqPredInfo>::iterator lit;
    for (lit = zzeqPredList.begin(); lit != zzeqPredList.end(); lit++)
      cout << (*lit).lhs_ << " " << (*lit).rhs_ << " ";
    cout << endl;
  }
}

void zzdetermineIntPredTypes(ListObj* const & formula)
{
  unsigned int prevSize = 0;
  while (zzintPredList.size() != prevSize)
  {
    prevSize = zzintPredList.size();
    list<ZZUnknownIntPredInfo>::iterator lit, remIt ;
    for (lit = zzintPredList.begin(); lit != zzintPredList.end(); lit++)
    {
      ZZUnknownIntPredInfo& uipi = (*lit);
      string lvarName = uipi.lhs_;
      string rvarName = uipi.rhs_;
	  string baseName = uipi.name_.substr(0, uipi.name_.find_last_of("_"));
      int lTypeId = zzgetVarTypeId(lvarName.c_str());
      int rTypeId = zzgetVarTypeId(rvarName.c_str());

      if (lTypeId > 0 && rTypeId > 0) //if both types are known
      {
        if (lTypeId != rTypeId)
          zzerr("The types of %s and %s on the left and right of "
                "an internal opreator must match.",
                lvarName.c_str(), rvarName.c_str());
        const char * typeName = zzdomain->getTypeName(lTypeId);
        string intPredName
          = PredicateTemplate::createInternalPredTypeName(baseName.c_str(),
                                                          typeName);
        formula->replace(uipi.name_.c_str(), intPredName.c_str());
        remIt = lit; lit++; zzintPredList.erase(remIt);
      }
      else  // if only one type is known
      if ( (lTypeId<=0 && rTypeId>0) || (lTypeId>0 && rTypeId<=0) )
      {
        int knownTypeId = (lTypeId>0) ? lTypeId : rTypeId;
        const char * typeName = zzdomain->getTypeName(knownTypeId);
        string intPredName
          = PredicateTemplate::createInternalPredTypeName(baseName.c_str(),
                                                          typeName);
        formula->replace(uipi.name_.c_str(), intPredName.c_str());
        const char* unknowVarName = (lTypeId>0) ?  rvarName.c_str() :
                                                   lvarName.c_str();
        zzvarNameToIdMap[unknowVarName].typeId_ = knownTypeId;
        remIt = lit; lit++; zzintPredList.erase(remIt);
      }
    }
  }
  if (zzintPredList.size() > 0)
  {
    zzerr("The following variables used with an internal operator have "
         "unknown types");
    list<ZZUnknownIntPredInfo>::iterator lit;
    for (lit = zzintPredList.begin(); lit != zzintPredList.end(); lit++)
      cout << (*lit).lhs_ << " " << (*lit).rhs_ << " ";
    cout << endl;
  }
}

void zzdetermineIntFuncTypes(ListObj* const & formula)
{
  unsigned int prevSize = 0;
  while (zzintFuncList.size() != prevSize)
  {
    prevSize = zzintFuncList.size();
    list<ZZUnknownIntFuncInfo>::iterator lit, remIt ;
    for (lit = zzintFuncList.begin(); lit != zzintFuncList.end(); lit++)
    {
      ZZUnknownIntFuncInfo& uifi = (*lit);
      Array<string> varNames = uifi.vnames_;
	  string baseName = uifi.name_.substr(0, uifi.name_.find_last_of("_"));

	  bool unknownTypes = false;
      Array<int> typeIds;
      for  (int i = 0; i < varNames.size(); i++)
      {
      	int typeId = zzgetVarTypeId(varNames[i].c_str());
      	typeIds.append(typeId);
		if (typeId <= 0)
		{
		  unknownTypes = true;
		}
      }

      if (!unknownTypes) //if both types are known
      {
        Array<string> typeNames;
        for (int i = 0; i < typeIds.size(); i++)
        {
          string typeName = zzdomain->getTypeName(typeIds[i]);
          typeNames.append(typeName);
        }
        string intPredFromFuncName
          = FunctionTemplate::createInternalFuncTypeName(baseName.c_str(),
                                                         typeNames);
        formula->replace(uifi.name_.c_str(), intPredFromFuncName.c_str());
        remIt = lit; lit++; zzintFuncList.erase(remIt);
      }
    }
  }
  if (zzintFuncList.size() > 0)
  {
    zzerr("The following variables used with an internal function have "
         "unknown types");
    list<ZZUnknownIntFuncInfo>::iterator lit;
    for (lit = zzintFuncList.begin(); lit != zzintFuncList.end(); lit++)
    {
      for (int i = 1; i < (*lit).vnames_.size(); i++)
       	cout << (*lit).vnames_[i] << " ";
    }
    cout << endl;
  }
}


bool zzcheckRightTypeAndGetVarId(const int& typeId, const char* const& varName,
                                 int& varId)
{
    // check that the variable is of the right type
  int expectedTypeId = -1;
  varId = zzgetVarId(varName, typeId, expectedTypeId);
  if (varId == 0)
  {
    const char* expName = zzdomain->getTypeName(typeId);
    const char* unexpName = zzdomain->getTypeName(expectedTypeId);
    zzerr("Variable %s is of the wrong type. Expected %s but given %s",
          varName, expName, unexpName);
    return false;
  }
  return true;
}

void zzaddType(const char* const& typeName,
               PredicateTemplate* const& predTemplate,
               FunctionTemplate* const& funcTemplate,
               bool isUnique, const Domain* const & domain)
{
  if (isUnique && funcTemplate != NULL)
  {
    zzerr("Function parameter (%s) cannot be existentially and uniquely "
          "quantified",typeName);
    isUnique = false;
  }

  if (predTemplate != NULL)
  {
    bool ok = predTemplate->appendTermType(typeName, isUnique, domain);
    if(!ok) zzexit("Term type %s should have been declared.", typeName);
  }
  else
  if (funcTemplate != NULL)
  {
    bool ok = funcTemplate->appendTermType(typeName, isUnique, domain);
    if (!ok) zzexit("Term type %s should have been declared.", typeName);
  }
}


int zzaddTypeToDomain(Domain* const & domain, const char* const & typeName)
{
  int typeId = domain->addType(typeName);

  if (typeName != PredicateTemplate::ANY_TYPE_NAME)
  {
      // create a PredicateTemplate to represent '=' (equality pred) for type
    string ptName = PredicateTemplate::createEqualPredTypeName(typeName);
    if (domain->getPredicateTemplate(ptName.c_str()) == NULL)
    {
      PredicateTemplate* pt = new PredicateTemplate();
      pt->setName(ptName.c_str());
      pt->appendTermType(typeName, false, domain);
      pt->appendTermType(typeName, false, domain);
      int id = domain->addPredicateTemplate(pt);
      zzassert(id >= 0, "expect pred template id >= 0");
      pt->setId(id);
    }

      // create a PredicateTemplate for each internal pred. for this type
/*
    Array<string> ptNames =
      PredicateTemplate::createInternalPredTypeNames(typeName);
	for (int i = 0; i < ptNames.size(); i++)
	{
	  string ptName = ptNames[i];
	  if (domain->getPredicateTemplate(ptName.c_str()) == NULL)
      {
      	PredicateTemplate* pt = new PredicateTemplate();
      	pt->setName(ptName.c_str());
      	pt->appendTermType(typeName, false, domain);
      	pt->appendTermType(typeName, false, domain);
      	int id = domain->addPredicateTemplate(pt);
      	zzassert(id >= 0, "expect pred template id >= 0");
      	pt->setId(id);
      }
	}
*/
  }

  return typeId;
}

void zzcreatePred(Predicate*& pred, const char* const & predName)
{
  const PredicateTemplate* t = zzdomain->getPredicateTemplate(predName);
  if (t==NULL)
  {
  	int index = zzfindInternalPredicate(predName);
  	// Internal predicates are declared on the fly
    if (index >= 0)
    {
      zzassert(zzdomain->getFunctionId(predName) < 0,
    	       "not expecting pred name to be declared as a function name");
  	  PredicateTemplate* ptemplate = new PredicateTemplate();
  	  ptemplate->setName(predName);

  	  // Add types
  	  for (int j = 1; j < zzinternalPredicates[index].size(); j++)
  	  {
  	    int id;
  	    const char* ttype = zzinternalPredicates[index][j];
  	    if (!zzdomain->isType(ttype))
  	    {
		  id = zzaddTypeToDomain(zzdomain, ttype);
  		  zzassert(id >= 0, "expecting var id >= 0");
  	    }
  	    zzaddType(ttype, ptemplate, NULL, false, zzdomain);
	    //delete [] ttype;
  	  }

   	  // Add template to domain
  	  zzassert(ptemplate, "not expecting ptemplate==NULL");
	  int id = zzdomain->addPredicateTemplate(ptemplate);
  	  zzassert(id >= 0, "expecting pred template id >= 0");
  	  ptemplate->setId(id);
	  zzassert(pred == NULL, "expect pred == NULL");
  	  pred = new Predicate(ptemplate);
  	  return;
    }
    else
  	  zzexit("Predicate %s should have been declared.", predName);
  }
    // commented out because when zzcreatePred is called predicate has already
    // been declared
  //if (t == NULL)
  //{
  //  zzerr("Failed to find predicate %s. Have you declared it?", predName);
  //    // create a fake predicate template and attempt to recover
  //  char buf[32];
  //  sprintf(buf, "%s%d", zzdefaultPredName, zzcount++);
  //  zzpredTemplate = new PredicateTemplate();
  //  zzpredTemplate->setDomain(zzdomain);
  //  zzpredTemplate->setName(buf);
  //  int id = zzdomain->addPredicateTemplate(zzpredTemplate);
  //  zzassert(id >= 0, "expect id >= 0");
  //  zzpredTemplate->setId(id);
  //  for (int i = 0; i < 20; i++)
  //  {
  //    sprintf(buf, "%s%d",zzdefaultTypeName, zzcount++);
  //    bool ok = zzpredTemplate->appendTermType(buf, false, zzdomain);
  //    if(!ok) zzexit("");
  //  }
  //  t = zzpredTemplate;
  //  zzpredTemplate = NULL;
  //}

  zzassert(pred == NULL, "expect pred == NULL");
  pred = new Predicate(t);
}



void zzcheckPredNumTerm(Predicate*& pred)
{
  int exp, unexp;
  if ((unexp=pred->getNumTerms()) != (exp=pred->getTemplate()->getNumTerms()))
  {
    zzerr("Wrong number of terms for predicate %s. Expected %d but given %d",
          pred->getName(), exp, unexp);

    char buf[128];
      // try to recover
    for (int i = unexp; i < exp; i++)
    {
      sprintf(buf, "%s%d", zzdefaultVarName, zzcount++);
      int typeId = pred->getTermTypeAsInt(i);
      int varId;
      bool rightType = zzcheckRightTypeAndGetVarId(typeId, buf, varId);
      if (!rightType) zzexit("");
      pred->appendTerm(new Term(varId, (void*)pred, true));
    }
  }
}


void zzpredAppendConstant(Predicate* const& pred, const int& constId,
                          const char* const & constName)
{
    // if exceeded the number of terms
  int exp, unexp;
  if ((unexp=pred->getNumTerms()) == (exp=pred->getTemplate()->getNumTerms()))
  {
    zzerr("Wrong number of terms for predicate %s. Expected %d but given >%d",
          pred->getName(), exp, unexp);
    return;
  }
/*
    // if this is not '=' predicate with unknown types
  if (!(strcmp(pred->getName(),PredicateTemplate::EQUAL_NAME) == 0) &&
  	  !(strcmp(pred->getTermTypeAsStr(pred->getNumTerms()),
               PredicateTemplate::ANY_TYPE_NAME) == 0))
  {
      // Check that constant has same type as that of predicate term
    int typeId = pred->getTermTypeAsInt(pred->getNumTerms());
    int unexpId;
    if (typeId != (unexpId=zzdomain->getConstantTypeId(constId)))
    {
      const char* expName = zzdomain->getTypeName(typeId);
      const char* unexpName = zzdomain->getTypeName(unexpId);
      zzerr("Constant %s is of the wrong type. Expected %s but "
            "given %s", constName, expName, unexpName);
      return;
    }
  }
*/
    // at this point, we have the right num of terms and right constant types
  if (pred != NULL) pred->appendTerm(new Term(constId, (void*)pred, true));
}


////////////////////////// function functions ////////////////////////

void zzconsumeToken(StrFifoList& tokenList, const char* c)
{
  const char* tok = tokenList.removeLast();
  if (strcmp(tok, c)!=0)
  {
    cout << "token = '" << tok << "', '" << c << "'" << endl;
    zzassert(strcmp(tok, c)==0, "expect strcmp(tok,c)==0");
  }
  delete [] tok;
}


void zzcreateFunc(Function*& func, const char* const & funcName)
{
  const FunctionTemplate* t = zzdomain->getFunctionTemplate(funcName);
  if (t==NULL)
  {
  	// Internal functions are declared on the fly
    int index;
	if ((index = zzfindInternalFunction(funcName)) >= 0)
 	{
      zzassert(zzfuncTemplate==NULL, "expecting zzfuncTemplate==NULL");
	  zzfuncTemplate = new FunctionTemplate();

	  // We are creating a new predicate as well
  	  zzassert(zzpredTemplate==NULL,"expecting zzpredTemplate==NULL");
  	  zzpredTemplate = new PredicateTemplate();

	  zzassert(zzdomain->getPredicateId(funcName) < 0,
    	       "not expecting func name to be declared as pred name");
  	  zzassert(zzfuncTemplate,"expecting zzfuncTemplate!=NULL");
	  zzfuncTemplate->setName(funcName);

	  // Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
	  char* predName;
	  predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
  		    					strlen(funcName) + 1)*sizeof(char));
 	  strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
	  strcat(predName, funcName);

	  // Check that predicate has not been declared a function
	  zzassert(zzdomain->getFunctionId(predName) < 0,
  		       "not expecting pred name to be declared as a function name");
  	  zzassert(zzpredTemplate,"expecting zzpredTemplate!=NULL");
 	  zzpredTemplate->setName(predName);
	  delete [] predName;

  	  // Add return type
  	  const char* retTypeName = zzinternalFunctions[index][1];

	  if (!zzdomain->isType(retTypeName))
  	  {
   	    int id = zzaddTypeToDomain(zzdomain, retTypeName);
        zzassert(id >= 0, "expecting retTypeName's id >= 0");
  	  }

	  zzfuncTemplate->setRetTypeName(retTypeName,zzdomain);
  	  // We are creating a new predicate as well
	  zzaddType(retTypeName, zzpredTemplate, NULL, false, zzdomain);

  	  // Add types
  	  for (int j = 2; j < zzinternalFunctions[index].size(); j++)
  	  {
  	    int id;
  	    const char* ttype = zzinternalFunctions[index][j];
  	    if (!zzdomain->isType(ttype))
  	    {
		  id = zzaddTypeToDomain(zzdomain, ttype);
  		  zzassert(id >= 0, "expecting var id >= 0");
  	    }
  	    zzaddType(ttype, zzpredTemplate, NULL, false, zzdomain);
	    // Add the type to the function too
	    zzaddType(ttype, NULL, zzfuncTemplate, false, zzdomain);
  	  }

	  // Add templates to domain
	  zzassert(zzfuncTemplate, "expecting zzfuncTemplate != NULL");
	  int id = zzdomain->addFunctionTemplate(zzfuncTemplate);
	  zzassert(id >= 0, "expecting function template's id >= 0");
	  zzfuncTemplate->setId(id);

	  zzassert(zzpredTemplate, "not expecting zzpredTemplate==NULL");
	  int predId = zzdomain->addPredicateTemplate(zzpredTemplate);
	  zzassert(predId >= 0, "expecting pred template id >= 0");
	  zzpredTemplate->setId(predId);

	  zzassert(func == NULL, "expect func == NULL");
  	  func = new Function(zzfuncTemplate);
	  zzfuncTemplate = NULL;
	  zzpredTemplate = NULL;
	  return;
	}
  	else
    	zzexit("Function %s should have been declared.", funcName);
  }
  //if (t == NULL)
  //{
  //  zzerr("Failed to find function %s. Have you declared it?", funcName);
  //    // create a fake predicate template and attempt to recover
  //  char buf[32];
  //  sprintf(buf, "%s%d", zzdefaultFuncName, zzcount++);
  //  zzfuncTemplate = new FunctionTemplate();
  //  zzfuncTemplate->setDomain(zzdomain);
  //  zzfuncTemplate->setRetTypeName(PredicateTemplate::ANY_TYPE_NAME);
  //  zzfuncTemplate->setName(buf);
  //  int id = zzdomain->addFunctionTemplate(zzfuncTemplate);
  //  zzassert(id >= 0, "expect id >= 0");
  //  zzfuncTemplate->setId(id);
  //  for (int i = 0; i < 20; i++)
  //  {
  //    sprintf(buf, "%s%d",zzdefaultTypeName, zzcount++);
  //    bool ok = zzfuncTemplate->appendTermType(buf, false, zzdomain);
  //    if(!ok) zzexit("");
  //  }
  //  t = zzfuncTemplate;
  //  zzfuncTemplate = NULL;
  //}

  zzassert(func == NULL, "expect func == NULL");
  func = new Function(t);
}


void zzcheckFuncNumTerm(Function*& func)
{
  int exp, unexp;
  if ((unexp=func->getNumTerms()) != (exp=func->getTemplate()->getNumTerms()))
  {
    zzerr("Wrong number of terms for func %s. Expected %d but given %d",
          func->getName(), exp, unexp);

    char buf[128];
      // try to recover
    for (int i = unexp; i < exp; i++)
    {
      sprintf(buf, "%s%d", zzdefaultVarName, zzcount++);
      int typeId = func->getTermTypeAsInt(i);
      int varId;
      bool rightType = zzcheckRightTypeAndGetVarId(typeId, buf, varId);
      if (!rightType) zzexit("");
      func->appendTerm(new Term(varId, (void*)func, false));
    }
  }
}


void zzfuncAppendConstant(Function* const& func, const int& constId,
                          const char* const & constName)
{
    // if exceeded the number of terms
  int exp, unexp;
  if ((unexp=func->getNumTerms()) == (exp=func->getTemplate()->getNumTerms()))
  {
    zzerr("Wrong number of terms for function %s. Expected %d but given > %d",
          func->getName(), exp, unexp);
    return;
  }
/*
  if (!(strcmp(func->getTermTypeAsStr(func->getNumTerms()),
               PredicateTemplate::ANY_TYPE_NAME)==0))
  {
	  // Check that constant has same type as that of predicate term
  	int typeId = func->getTermTypeAsInt(func->getNumTerms());
  	int unexpId;
  	if (typeId != (unexpId=zzdomain->getConstantTypeId(constId)))
  	{
      const char* expName = zzdomain->getTypeName(typeId);
      const char* unexpName = zzdomain->getTypeName(unexpId);
      zzerr("Constant %s is of the wrong type. Expected %s but given %s",
            constName, expName, unexpName);
      return;
  	}
  }
*/
    // at this point, we have the right num of term and right constant type
  if (func != NULL) func->appendTerm(new Term(constId, (void*)func, false));
}


/////////////////////// create clause from list obj//////////////////////////

void zzpermuteAsteriskedPreds(const int& numAsterisk,
                              const ListObj* const & formula,
                              const string& formulaStr,
                              Array<ListObj*>& clauses,
                              Array<string>& formulaStrs)
{
  clauses.clear();
  formulaStrs.clear();
  if (numAsterisk == 0)
  {
    clauses.append( new ListObj(formula));
    formulaStrs.append(formulaStr);
    return;
  }

  Array<int> astIdxs;
  for (unsigned int i = 0; i < formulaStr.length(); i++)
    if (formulaStr.at(i) == '*') astIdxs.append(i);
  assert(astIdxs.size() == numAsterisk);

    // add numAsterisk number of [false][true] to ArraysAccessor
  ArraysAccessor<bool> acc;
  for (int i = 0; i < numAsterisk; i++)
  {
    Array<bool>* a = new Array<bool>(2);
    a->append(false); a->append(true);
    acc.appendArray(a);
  }

  Array<bool> bArr;
  while (acc.getNextCombination(bArr))
  {
      // create a copy of the formula
    clauses.append(new ListObj(formula));
    int idx = 0;
    clauses[clauses.size()-1]->replaceAsterisk(bArr, idx);

    string s = formulaStr;
    assert(bArr.size() == astIdxs.size());
    for (int j = 0; j < bArr.size(); j++)
      s.at(astIdxs[j]) = (bArr[j]) ? ' ' : '!';

    formulaStrs.append(s);
  }

  acc.deleteArraysAndClear();
}


void zzgetDisjunctions(const ListObj* const & lo, Array<ListObj*>& clauses)
{
  const Array<ListObj*>& lobjs = lo->getList();

  if ((lobjs[0]->getStr())[0] != '^')
  {
    clauses.append((ListObj*)lo);
    return;
  }

  for (int i = 1; i < lobjs.size(); i++)
    clauses.append(lobjs[i]);
}

  // Checks if name starts with upper case or " (string constant)
const bool zzisConstant(const char* const & name)
{
  return (isupper(name[0]) || name[0] == '"');
}

Function* zzcreateFunc(const ListObj* const & lo)
{
  const Array<ListObj*>& termlo = lo->getList();
  const char* funcName = termlo[0]->getStr();
  Function* func = NULL;
  zzcreateFunc(func, funcName);
  for (int i = 1; i < termlo.size(); i++)
  {
    if (termlo[i]->isStr())  // if is a constant or variable
    {
      const char* name = termlo[i]->getStr();
      //if (isupper(name[0]))  // if is a constant
      if (zzisConstant(name))  // if is a constant
      {
        int constId = zzdomain->getConstantId(name);
        if (constId < 0)
          zzexit("zzcreateFunc(): failed to find constant %s. "
                 "Have you declared it?", name);
        zzfuncAppendConstant(func, constId, name);
      }
      else  // is a variable
      {
        if (func->getNumTerms() == func->getTemplate()->getNumTerms())
          zzexit("zzcreateFunc(): Function %s has too many terms",
                 func->getName());

          // check the type of the term that is to be added
        int typeId = func->getTermTypeAsInt(func->getNumTerms());
        int expectedTypeId;
        int varId = zzgetVarId(name, typeId, expectedTypeId);

        if (varId==0)
          zzexit("zzcreateFunc(): failed to create term, variable %s has wrong "
                 "type", name);
        func->appendTerm(new Term(varId, (void*)func, false));
      }
    }
    else // is a function
    {
        //push onto stack
      Function* termFunc = zzcreateFunc(termlo[i]);
      Term* newTerm = new Term(termFunc, (void*)func, false);
      termFunc->setParent(newTerm);
      func->appendTerm(newTerm);
    }
  }

  zzcheckFuncNumTerm(func);
  return func;
}


Predicate* zzcreatePred(const ListObj* const & lo)
{
  const Array<ListObj*>& termlo = lo->getList();
  const char* predName = termlo[0]->getStr();
  Predicate* pred = NULL;
  zzcreatePred(pred, predName);
  for (int i = 1; i < termlo.size(); i++)
  {
    if (termlo[i]->isStr())  // if is a constant or variable
    {
      const char* name = termlo[i]->getStr();
      if (zzisConstant(name))  // if is a constant
      {
        int constId = zzdomain->getConstantId(name);
        if (constId < 0)
          zzexit("zzcreatePred(): failed to find constant %s. "
                 "Have you declared it?", name);
        zzpredAppendConstant(pred, constId, name);
      }
      else  // is a variable
      {
        if (pred->getNumTerms() == pred->getTemplate()->getNumTerms())
          zzexit("zzcreatePred(): Predicate %s has too many terms",
                 pred->getName());

          // check the type of the term that is to be added
        int typeId = pred->getTermTypeAsInt(pred->getNumTerms());
        int expectedTypeId;
        int varId = zzgetVarId(name, typeId, expectedTypeId);

        if (varId == 0)
          zzexit("zzcreatePred(): failed to create term, variable %s has wrong "
                 "type", name);
        pred->appendTerm(new Term(varId, (void*)pred, true));
      }
    }
    else // is a function
    {
      Function* func = zzcreateFunc(termlo[i]);
      Term* newTerm = new Term(func, (void*)pred, true);
      func->setParent(newTerm);
      pred->appendTerm(newTerm);
    }
  }

  zzcheckPredNumTerm(pred);
  return pred;
}


void zzcreateClause(const ListObj* const & lo, Clause* const & clause,
                    const bool& isIndivisible)
{
  if (!isIndivisible)
  {
    zzvarCounter = 0;
    zzvarNameToIdMap.clear();
  }

  const Array<ListObj*>& clauselo = lo->getList();
    // Non-unit clause
  if (strcmp(clauselo[0]->getStr(), "v")==0)
  {
    for (int i = 1; i < clauselo.size(); i++)
    {
      const Array<ListObj*>& predlo = clauselo[i]->getList();
      Predicate* pred;

      if ((predlo[0]->getStr())[0] == '!')
      {
        pred = zzcreatePred(predlo[1]);
        pred->setSense(false);
      }
      else
        pred = zzcreatePred(clauselo[i]);
      pred->setParent(clause);
      clause->appendPredicate(pred);
    }
  }
    // Unit clause
  else
  {
    Predicate* pred;
    if (((*lo)[0]->getStr())[0] == '!')
    {
      pred = zzcreatePred((*lo)[1]);
      pred->setSense(false);
    }
    else
      pred = zzcreatePred(lo);
    pred->setParent(clause);
    clause->appendPredicate(pred);
  }

  zzcheckVarNameToIdMap();
}


  // clauses are those that occur together in CNF
void zzcreateClauses(const ListObj* const & lo, Array<Clause*>& clauses,
                     Clause*& flippedClause, const bool& isIndivisible)
{
  zzvarCounter = 0;
  zzvarNameToIdMap.clear();
  flippedClause = NULL;
    // clauseOfUnitPreds contains the predicates of unit clauses
    // e.g if the cnf formula is P(x) ^ Q(x) ^ (P(y) v Q(y))
    // then clauseOfUnitPreds is !P(x) v !Q(x)
  Clause* clauseOfUnitPreds = new Clause;
  ListObj* unitPreds = new ListObj; ListObj orr("v"); unitPreds->append(&orr);
  Array<ListObj*> disjunctions;
  zzgetDisjunctions(lo, disjunctions);
  for (int i = 0; i < disjunctions.size(); i++)
  {
    Clause* clause = new Clause();
    zzcreateClause(disjunctions[i], clause, isIndivisible);
    if (clause->getNumPredicates() > 1)
      clauses.append(clause);
    else
    {
      unitPreds->append(disjunctions[i]);
      delete clause;
    }
  }

  if (unitPreds->size() > 1) zzcreateClause(unitPreds, clauseOfUnitPreds,
                                            isIndivisible);
  unitPreds->clear();
  delete unitPreds;

  if (clauseOfUnitPreds->getNumPredicates() > 1)
  {
    for (int i = 0; i < clauseOfUnitPreds->getNumPredicates(); i++)
      ((Predicate*)clauseOfUnitPreds->getPredicate(i))->invertSense();
    clauses.append(clauseOfUnitPreds);
    flippedClause = clauseOfUnitPreds;
  }
  else
  if (clauseOfUnitPreds->getNumPredicates() == 1)
  {
      //if these is only one unit pred, then don't invert its sense
    clauses.append(clauseOfUnitPreds);
  }
  else
    delete clauseOfUnitPreds;
}


/**
 * Creates blocks in a domain based on existentially and uniquely quantified
 * variables (the ! operator). All predicates are examined if they have been marked
 * as block predicates.
 *
 * @param domain Domain in which the blocks are created.
 *
 * @return Number of blocks created.
 */
int zzcreateBlocks(const Domain* const & domain)
{
  int totalNumPreds = 0;
  int numFOPreds = domain->getNumPredicates();
  for (int p = 0; p < numFOPreds; p++)
  {
    const PredicateTemplate* pt = domain->getPredicateTemplate(p);
    const Array<int>* uniqueVarIndexes = pt->getUniqueVarIndexes();
      // If predicate has no blocked vars, then continue
    if (uniqueVarIndexes->size() == 0) continue;

    Predicate* pred = domain->createPredicate(p, false);
      // Save variable ids, set unique vars to dummy id, ground pred to generate
      // blocks, then set var ids back to original and add as block to domain
    Array<int> uniqueVarIds;
      // Save var ids
    for (int i = 0; i < pred->getNumTerms(); i++)
    {
      if (uniqueVarIndexes->contains(i))
        uniqueVarIds.append(pred->getTerm(i)->getId());
    }
      // Set dummy id
    for (int i = 0; i < uniqueVarIndexes->size(); i++)
    {
      ((Term*)pred->getTerm((*uniqueVarIndexes)[i]))->setId(0);
    }
      // Ground pred to generate blocks
    Array<Predicate*> predArr;
    pred->createAllGroundings(domain, predArr);
    int numPreds = predArr.size();
    totalNumPreds += numPreds;

    for (int i = 0; i < numPreds; i++)
    {
      Predicate* newPred = predArr[i];
        // Set var ids back to original
      for (int j = 0; j < uniqueVarIndexes->size(); j++)
      {
        Term* t = (Term*)newPred->getTerm((*uniqueVarIndexes)[j]);
        t->setId(uniqueVarIds[j]);
      }
        // Add as block to domain
      int blockIdx = domain->addPredBlock(newPred);

      bool trueOne = false;
        // If groundings of this pred occur, then make sure exactly one is true
        // and tell this to the domain
      if ((zzpredIdToGndPredMap.find(pred->getId())) !=
          zzpredIdToGndPredMap.end())
      {
        PredicateHashArray* pha = zzpredIdToGndPredMap[pred->getId()];
        for (int j = 0; j < pha->size(); j++)
        {
          Predicate* gndPred = (*pha)[j];
            // Only one atom in a block can be true
          if (gndPred->getTruthValue() == TRUE &&
              newPred->canBeGroundedAs(gndPred))
          {
            if (domain->getBlockEvidence(blockIdx))
              zzexit("More than one true atom found for mutually "
                     "exclusive and exhaustive variables");
            domain->setBlockEvidence(blockIdx, true);
            domain->setTruePredInBlock(blockIdx, new Predicate(*gndPred));
            trueOne = true;
          }
        }
      }
        // Query pred: There does not have to be a true one
      else
        trueOne = true;

        // One pred has to be true
      if (!trueOne)
      {
      	// This assumes that all groundings of predicate are either query or
      	// evidence. It doesn't work when some groundings are query, some are
      	// evidence.
        //cout << "Problem with predicate ";
        //newPred->print(cout, domain);
        //cout << endl;
        //zzexit(": No true atom was found for mutually "
        //       "exclusive and exhaustive variables");
      }
    }
    delete pred;
  }
  return totalNumPreds;
}


//////////create formulas by grounding variables preceded by a plus///////////

void zzgroundPlusVar(const ListObj* const & formula, const string& formulaStr,
                     const StringToIntMap& varNameToTypeIdMap,
                     Array<ListObj*>& formulas, Array<string>& formulaStrs,
                     const Domain* const & domain,const Domain* const & domain0)
{
  formulas.clear();
  formulaStrs.clear();
  if (varNameToTypeIdMap.size()==0)
  {
    formulas.append(new ListObj(formula));
    formulaStrs.append(formulaStr);
    return;
  }

  Array<Array<int>*> cleanUp;
  ArraysAccessor<int> acc;
  Array<string> varNames;
  StringToIntMap::const_iterator mit = varNameToTypeIdMap.begin();
  for (; mit != varNameToTypeIdMap.end(); mit++)
  {
    int typeId = (*mit).second;
    zzassert(typeId > 0, "expect typeId > 0");

    Array<int>* constArr;
    constArr = (Array<int>*) domain->getConstantsByType(typeId);

    acc.appendArray(constArr);
    varNames.append((*mit).first);
  }

  Array<int> constIds;
  while (acc.getNextCombination(constIds))
  {
    ListObj* gndFormula = new ListObj(formula);
    string s = formulaStr;

    zzassert(constIds.size() == varNames.size(),
             "expect constIds.size() == varNames.size()");
    for (int i = 0; i < varNames.size(); i++)
    {
      const char* constName = domain->getConstantName(constIds[i]);
      ListObj::replace(gndFormula, varNames[i].c_str(), constName, domain);
      unsigned int a = s.find("+" + varNames[i]);
      assert(a != string::npos);
      s.replace(a, varNames[i].length() + 1, constName);
    }
    formulas.append(gndFormula);
    formulaStrs.append(s);
  }
  //acc.deleteArraysAndClear();

  if (domain0) cleanUp.deleteItemsAndClear();
}

////////////////////////////// misc //////////////////////////////////


void zzcreateListObjFromTop(stack<ListObj*>& stack, const char* const & op)
{
  //zzassert(zzformulaListObjs.size()>=1, "expect zzformulaListObjs.size()>=1");
  zzassert(stack.size() >= 1, "expect stack.size()>=1");
  ListObj* lo1 = stack.top(); stack.pop();
  ListObj* lo = new ListObj; lo->append(op); lo->append(lo1);
  stack.push(lo);
}


void zzcreateListObjFromTopTwo(stack<ListObj*>& stack, const char* const & op)
{
  //zzassert(zzformulaListObjs.size()>=2,"expect zzformulaListObjs.size()>=2");
  zzassert(stack.size()>=2,"expect stack.size()>=2");
  ListObj* lo1 = stack.top(); stack.pop();
  ListObj* lo2 = stack.top(); stack.pop();

  if ((strcmp(op,"v")==0 && lo2->hasOrOp()) ||
      (strcmp(op,"^")==0 && lo2->hasAndOp()))
  {
    lo2->append(lo1);
    stack.push(lo2);
  }
  else
  {
    ListObj* lo = new ListObj; lo->append(op); lo->append(lo2); lo->append(lo1);
    stack.push(lo);
  }
}


void zzcreateListObjFromTopThree(stack<ListObj*>& stack)
{
  //zzassert(zzformulaListObjs.size()>=3, "expect zzformulaListObjs.size()>=3");
  zzassert(stack.size()>=3, "expect stack.size()>=3");
  ListObj* lo1 = stack.top(); stack.pop();
  ListObj* lo2 = stack.top(); stack.pop();
  ListObj* lo3 = stack.top(); stack.pop();
  ListObj* lo = new ListObj; lo->append(lo3); lo->append(lo2); lo->append(lo1);
  stack.push(lo);
}


void zzcreateIntConstant(char* const & buf, const char* const & typeName,
                       const int& i)
{ sprintf(buf, "C@%s@%d", typeName, i); }

  // Checks all types of domain if C@type@intStr is in domain
bool isIntConstant(const int& i, const Domain* const & domain)
{
  const Array<const char*>* typeNames = domain->getTypeNames();
  for (int j = 0; j < typeNames->size(); j++)
  {
  	char constName[100];
  	zzcreateIntConstant(constName, (*typeNames)[j], i);
  	if (domain->isConstant(constName))
  	{
  	  return true;
  	}
  }
  return false;
}

  // Returns the first type found to have C@type@intStr as a constant
const char* getIntConstantTypeName(const int& i, const Domain* const & domain)
{
  const Array<const char*>* typeNames = domain->getTypeNames();
  for (int j = 0; j < typeNames->size(); j++)
  {
  	char constName[100];
  	zzcreateIntConstant(constName, (*typeNames)[j], i);
  	if (domain->getConstantId(constName) >= 0) return (*typeNames)[j];
  }
  return NULL;
}

void zzcreateAndCheckNumConstant(const char* const & intStr,
                                 const Function* const & func,
                                 const Predicate* const & pred,
                                 const Domain* const & domain,
                                 char* constName)
{
  double d = atof(intStr); int i = int(d);
  //if (d!=i) zzerr("%s cannot be a term. Only integer terms are allowed",intStr);

  const char* typeName = NULL;
  if (func) typeName = func->getTermTypeAsStr(func->getNumTerms());
  else      typeName = pred->getTermTypeAsStr(pred->getNumTerms());

  if (typeName == NULL)
  { zzerr("Too many terms for predicate/function"); constName = NULL; return;}

	// If type name is still open, then try to determine it
  if (strcmp(typeName, PredicateTemplate::ANY_TYPE_NAME)==0)
  {
  	  // Constant may have been previously declared
  	if (isIntConstant(i, domain))
	  typeName = getIntConstantTypeName(i, domain);
  }

  zzcreateIntConstant(constName, typeName, i);

  char buf[30]; sprintf(buf,"%f",d);
  if (zzconstantMustBeDeclared && domain->getConstantId(constName) < 0)
    zzerr("Constant %s must be declared before it is used", buf);
}


  //ASSUMPTION: users don't define truth values of '=' ground preds e.g. A=A
void zzaddGndPredsToDb(Database* const & db)
{
    // Add explicit evidence to db
  int numPreds = zzdomain->getNumPredicates();
  hash_map<int, PredicateHashArray*>::iterator it;
  for (int i = 0; i < numPreds; i++)
  {
    if ((it = zzpredIdToGndPredMap.find(i)) != zzpredIdToGndPredMap.end())
    {
      PredicateHashArray* predHashArray = (*it).second;
      for (int j = 0; j < predHashArray->size(); j++)
      {
        db->addEvidenceGroundPredicate((*predHashArray)[j]);
        double rv = (*predHashArray)[j]->getRealValue();
        if (rv > numeric_limits<double>::min())
          db->setRealValue((*predHashArray)[j], rv);
      }

      predHashArray->deleteItemsAndClear();
    }
    else
    {
      //  '=' predicates are handled specially by database
    }
  }

    // If the predicate occurs in the mln with a non-evidence atom, then add
    // it to the index in DB

    // Keep track of preds already indexed
  Array<Predicate*> indexedPreds;

  for (int i = 0; i < zzmln->getNumClauses(); i++)
  {
    const Clause* clause = zzmln->getClause(i);
      // First check if non-evid. pred is in clause
    Array<bool> nonEvidPred(clause->getNumPredicates(), false);
    bool oneNonEvidPred = false;
    for (int j = 0; j < clause->getNumPredicates(); j++)
    {
      Predicate* pred = clause->getPredicate(j);
      if (!db->isClosedWorld(pred->getId()))
      {
        nonEvidPred[j] = true;
        oneNonEvidPred = true;
      }
    }

      // If at least one pred is non-evid., then create index for evidence
    if (oneNonEvidPred)
    {
      for (int j = 0; j < clause->getNumPredicates(); j++)
      {
        if (!nonEvidPred[j])
        {
          Predicate* pred = clause->getPredicate(j);
          if (pred->isEqualPred()) continue;
            // Neg. literal means true groundings are added to index which
            // already happened above in addEvidenceGroundPredicate
          if (!pred->getSense())
            continue;

          for (int k = 0; k < indexedPreds.size(); k++)
          {
            if (indexedPreds[k]->canBeGroundedAs(pred))
              continue;
          }
            // Add all groundings to index
          indexedPreds.append(pred);
            // Generate groundings to add to index
          Array<Predicate*> predArr;
          pred->createAllGroundings(zzdomain, predArr);
          int numPreds = predArr.size();
          for (int l = 0; l < numPreds; l++)
          {
            Predicate* newPred = predArr[l];
            db->addPredToEvidenceIndex(newPred, pred->getSense());
            delete newPred;
          }
        }
      }
    }
  }

  for (unsigned int i = 0; i < zzpredIdToGndPredMap.size(); i++)
    delete zzpredIdToGndPredMap[i];
}


void zzcreateBoolArr(int idx, Array<bool>*& curArray,
                     Array<Array<bool>*>& boolArrays)
{
  --idx;

  Array<bool>* copyArray = new Array<bool>(*curArray);

  curArray->append(true);
  copyArray->append(false);

  if (idx == 0)
  {
    boolArrays.append(curArray);
    boolArrays.append(copyArray);
  }
  else
  {
    zzcreateBoolArr(idx, curArray, boolArrays);
    zzcreateBoolArr(idx, copyArray, boolArrays);
  }
}


  // vs (variable or string) is the name of the constant
void zzaddConstantToDomain(const char* const & vs, const char* const & typeName)
{
  //if it is not a string and it does not begin with an uppercase char
  //if (vs[0] != '"' && !isupper(vs[0]))
  if (!zzisConstant(vs))
  {
    zzerr("Constant %s must begin in uppercase char or be a \"string\".", vs);
    return;
  }

  zzassert(typeName != NULL, "expect typeName != NULL");
  zzdomain->addConstant(vs, typeName);
  //if (id < 0) zzerr("Failed to add constant %s", vs);
}


void zzaddConstantToPredFunc(const char* const & constName)
{
    //commented out because a constant can be declared with its first appearance
  //int constId = zzcheckConstantAndGetId(constName);

  const char* typeName = NULL;
  if (zzfunc) typeName = zzfunc->getTermTypeAsStr(zzfunc->getNumTerms());
  else
  if (zzpred) typeName = zzpred->getTermTypeAsStr(zzpred->getNumTerms());

    // May be continuing after a parse error
  if (typeName == NULL)
  {
    zzwarn("Wrong number of terms.");
    typeName = PredicateTemplate::ANY_TYPE_NAME;
  }

  zzaddConstantToDomain(constName, typeName);
  int constId = zzdomain->getConstantId(constName);
  if (zzfunc) zzfuncAppendConstant(zzfunc, constId, constName);
  else if (zzpred) zzpredAppendConstant(zzpred, constId, constName);
  else zzexit("No predicate or function is defined.");
}


void zztermIsConstant(const char* const & constName,
                      const char* const & constStr, const bool& appendToFormula)
{
  int constId = zzdomain->getConstantId(constName);
    //commented out because a constant can be declared with its first appearance
  //if (constId < 0) zzexit("Failed to find constant %s. Have you declared it?",
  //                        constName);
  if (constId < 0)
  {
    const char* typeName = NULL;
    if (zzfunc) typeName = zzfunc->getTermTypeAsStr(zzfunc->getNumTerms());
    else
    if (zzpred) typeName = zzpred->getTermTypeAsStr(zzpred->getNumTerms());

      // May be continuing after a parse error
    if (typeName==NULL)
    {
      zzwarn("Wrong number of terms.");
      typeName=PredicateTemplate::ANY_TYPE_NAME;
    }

    zzaddConstantToDomain(constName, typeName);
    constId = zzdomain->getConstantId(constName);
  }

    //always check zzfunc first, as a function can be found inside a predicate
  if (zzfunc != NULL)
  {
    zzfuncAppendConstant(zzfunc, constId, constName);
    zzpredFuncListObjs.top()->append(constName);
  }
  else
  if (zzpred != NULL)
  {
    zzpredAppendConstant(zzpred, constId, constName);
    zzassert(zzpredFuncListObjs.size()==1,
             "expect zzpredFuncListObjs.size()==1");
    zzpredFuncListObjs.top()->append(constName);
    if (appendToFormula) zzformulaStr.append(constStr);
  }
  else
    zzexit("No function or predicate to hold constant %s", constName);
}


/**
 * Append a variable to a predicate
 *
 * @varName The name of the variable being appended
 */
void zzputVariableInPred(const char* varName, const bool& folDbg)
{
  if (folDbg >= 1) printf("v_%s ", varName);

  ++zzfdnumVars;
  string newVarName = zzgetNewVarName(varName);

  if (zzpred != NULL)
  {
    bool rightNumTerms = true;
    bool rightType = true;
    int exp, unexp;

      // check that we have not exceeded the number of terms
    if ((unexp = zzpred->getNumTerms()) ==
       	(exp = zzpred->getTemplate()->getNumTerms()))
    {
      rightNumTerms = false;
      zzerr("Wrong number of terms for predicate %s. "
            "Expected %d but given %d", zzpred->getName(), exp, unexp+1);
    }

    int varId = -1;
    if (rightNumTerms)
    {
        // check that the variable is of the right type
      int typeId = zzpred->getTermTypeAsInt(zzpred->getNumTerms());
      rightType = zzcheckRightTypeAndGetVarId(typeId, newVarName.c_str(), varId);
    }

    if (rightNumTerms && rightType)
    {
      zzpred->appendTerm(new Term(varId, (void*)zzpred, true));
      zzpredFuncListObjs.top()->append(newVarName.c_str());
      //zzformulaStr.append(varName);
    }
  }
  else
    zzexit("No function or predicate to hold variable %s",varName);
}


void zztermIsVariable(const bool& folDbg)
{
  const char* varName = zztokenList.removeLast();

    // if it is a constant (starts in uppercase or a string)
  if (zzisConstant(varName))
  {
    if (folDbg >= 1) printf("c2_%s ", varName);

    if (zzconstantMustBeDeclared)
      zzerr("Constant %s must be declared before it is used", varName);
    zztermIsConstant(varName, varName, true);
    delete [] varName;
  }
  else
  {   //we are dealing with a variable that begins in lowercase
    if (folDbg >= 1) printf("v_%s ", varName);

    ++zzfdnumVars;
    string newVarName = zzgetNewVarName(varName);

      //always check zzfunc first, as a function can be found inside a predicate
    if (zzfunc != NULL)
    {
      bool rightNumTerms = true;
      bool rightType = true;
      int exp, unexp;

        // check that we have not exceeded the number of terms
      if ((unexp = zzfunc->getNumTerms()) ==
          (exp = zzfunc->getTemplate()->getNumTerms()))
      {
        rightNumTerms = false;
        zzerr("Wrong number of terms for function %s. "
              "Expected %d but given %d", zzfunc->getName(), exp, unexp+1);
      }

      int varId = -1;
      if (rightNumTerms)
      {
          // check that the variable is of the right type
        int typeId = zzfunc->getTermTypeAsInt(zzfunc->getNumTerms());
        rightType = zzcheckRightTypeAndGetVarId(typeId, newVarName.c_str(),
                                                varId);
      }

      if (rightNumTerms && rightType)
      {
        zzfunc->appendTerm(new Term(varId, (void*)zzfunc, false));
        zzpredFuncListObjs.top()->append(newVarName.c_str());
        //zzformulaStr.append(varName);
      }
    }
    else
    if (zzpred != NULL)
    {
      bool rightNumTerms = true;
      bool rightType = true;
      int exp, unexp;

        // check that we have not exceeded the number of terms
      if ((unexp = zzpred->getNumTerms()) ==
          (exp = zzpred->getTemplate()->getNumTerms()))
      {
        rightNumTerms = false;
        zzerr("Wrong number of terms for predicate %s. "
              "Expected %d but given %d", zzpred->getName(), exp, unexp+1);
      }

      int varId = -1;
      if (rightNumTerms)
      {
          // check that the variable is of the right type
        int typeId = zzpred->getTermTypeAsInt(zzpred->getNumTerms());
        rightType = zzcheckRightTypeAndGetVarId(typeId, newVarName.c_str(),
                                                varId);
      }

      if (rightNumTerms && rightType)
      {
        zzpred->appendTerm(new Term(varId, (void*)zzpred, true));
        if (!zzisHybrid)
        {
          if (zzpredFuncListObjs.size() != 1)
            zzerr("There may be a parse error. Have you declared all the "
                  "predicates and functions?");
          zzpredFuncListObjs.top()->append(newVarName.c_str());
        }
        else
        {
          zzcontPred->append(varName);
        }
        zzformulaStr.append(varName);
      }
    }
    else
      zzexit("No function or predicate to hold variable %s",varName);


    if (zzisPlus)
    {
      //zzisPlus = false; //commented out: set to false in not: rule
        // if variable is explicitly universally/existentially quantified
      if (!zzvarIsQuantified(varName)) // use the old var name
      {
          // we'll set it to the actual type when the entire formula is seen
        zzplusVarMap[newVarName] =  zzanyTypeId;
      }
      else
        zzerr("the '+' operator cannot be applied to variable %s that is "
              "explicitly universally/existentially quantified", varName);
    }
    delete [] varName;
  } //else we are dealing with a variable that begins in lowercase
}



void zzcleanUp()
{
  zzeqPredList.clear();
  zzintPredList.clear();
  zzintFuncList.clear();
  while (!zzinStack.empty()) zzinStack.pop();
  zzvarNameToIdMap.clear();
  zzfuncToFuncVarMap.clear();
  zzoldNewVarList.clear();
  zzplusVarMap.clear();
  zztokenList.deleteContentsAndClear();
  while (!zzfuncStack.empty()) zzfuncStack.pop();
  while (!zzfuncConjStack.empty()) zzfuncConjStack.pop();
  while (!zzformulaListObjs.empty())
  {
    ListObj* top = zzformulaListObjs.top();
    zzformulaListObjs.pop();
    delete top;
  }
  while (!zzpredFuncListObjs.empty())
  {
    ListObj* top = zzpredFuncListObjs.top();
    zzpredFuncListObjs.pop();
    delete top;
  }
    //PredicateHashArray and contents deleted in zzaddGndPredsToDb()
  zzpredIdToGndPredMap.clear();
  zzformulaInfos.clear();
}


void zzinit()
{
  zzafterRtParen = false;
  zzcount = 0;
  zzline = 0;
  zzcolumn = -1;
  zznumCharRead = 0;
  zznumErrors = 0;
  zzok = true;
  zzmln = NULL;
  zzdomain = NULL;
  zznumEofSeen = 0;
  zzeqTypeCounter = 0;
  zzintPredTypeCounter = 0;
  zzintFuncTypeCounter = 0;
  zzanyTypeId = -1;
  zzerrMsg[0] = '\0';
  zzfdfuncConstants.clear();
  zzusingLinkedFunctions = false;
  zztmpReturnNum = false;

  // Add internal predicates
  Array<const char*>* pred;
  pred = new Array<const char*>;
  pred->append("greaterThan");
  //pred->append("int");
  //pred->append("int");
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalPredicates.append(*pred);
  delete pred;

  pred = new Array<const char*>;
  pred->append("lessThan");
  //pred->append("int");
  //pred->append("int");
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalPredicates.append(*pred);
  delete pred;

  pred = new Array<const char*>;
  pred->append("greaterThanEq");
  //pred->append("int");
  //pred->append("int");
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalPredicates.append(*pred);
  delete pred;

  pred = new Array<const char*>;
  pred->append("lessThanEq");
  //pred->append("int");
  //pred->append("int");
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalPredicates.append(*pred);
  delete pred;

  pred = new Array<const char*>;
  pred->append("substr");
  //pred->append("string");
  //pred->append("string");
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  pred->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalPredicates.append(*pred);
  delete pred;

  // Add internal functions
  Array<const char*>* func;

  func = new Array<const char*>;
  func->append("succ");
  //func->append("int"); //return type
  //func->append("int");
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalFunctions.append(*func);
  delete func;

  func = new Array<const char*>;
  func->append("plus");
  //func->append("int"); //return type
  //func->append("int");
  //func->append("int");
    // return type
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalFunctions.append(*func);
  delete func;

  func = new Array<const char*>;
  func->append("minus");
  //func->append("int"); //return type
  //func->append("int");
  //func->append("int");
    // return type
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalFunctions.append(*func);
  delete func;

  func = new Array<const char*>;
  func->append("times");
  //func->append("int"); //return type
  //func->append("int");
  //func->append("int");
    // return type
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalFunctions.append(*func);
  delete func;

  func = new Array<const char*>;
  func->append("dividedBy");
  //func->append("int"); //return type
  //func->append("int");
  //func->append("int");
    // return type
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalFunctions.append(*func);
  delete func;

  func = new Array<const char*>;
  func->append("mod");
  //func->append("int"); //return type
  //func->append("int");
  //func->append("int");
    // return type
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalFunctions.append(*func);
  delete func;

  func = new Array<const char*>;
  func->append("concat");
  //func->append("string"); //return type
  //func->append("string");
  //func->append("string");
    // return type
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  func->append(PredicateTemplate::ANY_TYPE_NAME);
  zzinternalFunctions.append(*func);
  delete func;
}


void zzreset()
{
  zzvarCounter = 0;
  zzscopeCounter = 0;
  zzoldNewVarList.clear();
  zzvarNameToIdMap.clear();
  zzfuncToFuncVarMap.clear();
  zzplusVarMap.clear();
  zzeqPredList.clear();
  zzintPredList.clear();
  zzintFuncList.clear();

  zztypeName = NULL;
  zzpredTemplate = NULL;
  zzfuncTemplate = NULL;
  zzpred = NULL;
  zzfunc = NULL;
  while (!zzfuncStack.empty()) zzfuncStack.pop();
  while (!zzfuncConjStack.empty()) zzfuncConjStack.pop();
  if (zzwt) { delete zzwt; zzwt = NULL; }
  if (zzutil) { delete zzutil; zzutil = NULL; }
  if (zzrealValue) { delete zzrealValue; zzrealValue = NULL; }
  zzisNegated = false;
  zzisAsterisk = false;
  zzisPlus = false;
  zzhasFullStop = false;
  zzhasWeightFullStop = false;
  zzinIndivisible = false;
  zzisHybrid = false;
  zznumAsterisk = 0;
  zztrueFalseUnknown = 't';
  zzformulaStr.clear();

  zzfuncConjStr.clear();
  zzparseGroundPred = false;
  while (!zzformulaListObjs.empty())
  {
    ListObj* top = zzformulaListObjs.top();
    zzformulaListObjs.pop();
    delete top;
  }
  while (!zzpredFuncListObjs.empty())
  {
    ListObj* top = zzpredFuncListObjs.top();
    zzpredFuncListObjs.pop();
    delete top;
  }
  while (!zzfuncStack.empty()) zzfuncStack.pop();
  while (!zzfuncConjStack.empty()) zzfuncConjStack.pop();

  zzfdnumPreds = 0;
  zzfdnumFuncs = 0;
  zzfdnumVars = 0;
//  zzfdisEqualPred = false;
  zzfdfuncName.clear();
  zzfdfuncConstants.clear();
  zzfdconstName.clear();
  zztmpReturnNum = false;
  zzinfixPredName = NULL;
  zzinfixFuncName = NULL;
}


string zzappend(const char* const & s, const int& i)
{
  char buf[16];
  sprintf(buf,"%d",i);
  string str;
  return str.append(s).append(buf);
}

string zzappendWithUnderscore(const char* const & s, const int& i)
{
  char buf[16];
  sprintf(buf,"%d",i);
  string str;
  return str.append(s).append("_").append(buf);
}

void zzcheckAllTypesHaveConstants(const Domain* const & domain)
{
  const Array<const char*>* types = domain->getTypeNames();
  for (int i = 0; i < types->size(); i++)
  {
    if (strcmp((*types)[i],PredicateTemplate::ANY_TYPE_NAME)==0) continue;
    if (strcmp((*types)[i],PredicateTemplate::INT_TYPE_NAME)==0) continue;
    if (strcmp((*types)[i],PredicateTemplate::STRING_TYPE_NAME)==0) continue;
    if (domain->getNumConstantsByType((*types)[i]) <= 0)
      zzerr("type %s has no constant. A type must have at least one constant",
            (*types)[i]);
  }
}


void zzfillClosedWorldArray(Array<bool>& isClosedWorldArr,
                            const bool& allPredsExceptQueriesAreClosedWorld,
                            const StringHashArray* const & openWorldPredNames,
                            const StringHashArray* const & closedWorldPredNames,
                            const StringHashArray* const & queryPredNames)
{
  if (queryPredNames)
  {
    for (int i = 0; i < queryPredNames->size(); i++)
    {
      const char* predName = (*queryPredNames)[i].c_str();
      const PredicateTemplate* pt = zzdomain->getPredicateTemplate(predName);
      if (pt == NULL)
      {
        zzerr("Query predicate %s is not found. Please declare it. "
              "Note that '!' and '?' should not be used with query predicates.",
              predName);
        continue;
      }
      if (pt->isEqualPredicateTemplate())
      {
        zzerr("'=' predicate cannot be a query predicate()");
        exit(-1);
      }
    }
  }

  int numPreds = zzdomain->getNumPredicates();
  isClosedWorldArr.growToSize(numPreds, true);
  if (!allPredsExceptQueriesAreClosedWorld)
  {
      // If a predicate has no evidence atoms, it is open-world (unless it's in
      // cwPredNames), if it has evidence atoms, it is closed-world (unless it's
      // in owPredNames).
    for (int i = 0; i < numPreds; i++)
    {
      hash_map<int, PredicateHashArray*>::iterator it;
      for (int i = 0; i < numPreds; i++)
      {
        if ((it = zzpredIdToGndPredMap.find(i)) != zzpredIdToGndPredMap.end())
        {
            // At least one evidence grounding is present
          isClosedWorldArr[i] = true;
        }
        else
        {
            // equality and internal predicates are handled specially by
            // database
          const PredicateTemplate* pt = zzdomain->getPredicateTemplate(i);
          if (!pt->isEqualPredicateTemplate() &&
              !pt->isInternalPredicateTemplate())
            isClosedWorldArr[i] = false;
          else
            isClosedWorldArr[i] = true;
        }
      }
    }
  }

    // Force these to be open-world
  if (openWorldPredNames)
  {
    for (int i = 0; i < openWorldPredNames->size(); i++)
    {
      const char* predName = (*openWorldPredNames)[i].c_str();
      int predId = zzdomain->getPredicateId(predName);
      isClosedWorldArr[predId] = false;
    }
  }
    // Force these to be closed-world
  if (closedWorldPredNames)
  {
    for (int i = 0; i < closedWorldPredNames->size(); i++)
    {
      const char* predName = (*closedWorldPredNames)[i].c_str();
      int predId = zzdomain->getPredicateId(predName);
      isClosedWorldArr[predId] = true;
    }
  }
    // Queries are always open-world
  if (queryPredNames)
  {
    for (int i = 0; i < queryPredNames->size(); i++)
    {
      const char* predName = (*queryPredNames)[i].c_str();
      int predId = zzdomain->getPredicateId(predName);
      isClosedWorldArr[predId] = false;
    }
  }
}


void zzappendUnitClausesToMLN(const Domain* const & domain, MLN* const & mln,
                              const double& defaultWt )
{
  for (int i = 0; i < domain->getNumPredicates(); i++)
  {
    Predicate* pred = domain->createPredicate(i, false);
    if (pred == NULL) continue;
    Clause* clause = ClauseFactory::createUnitClause(pred, false);
    delete pred;

    if (clause == NULL) continue;
    if (mln->containsClause(clause)) { delete clause; continue; }

    int idx;
    ostringstream oss;
    clause->getPredicate(0)->getTemplate()->printWithStrVar(oss);
    bool app = mln->appendClause(oss.str(), false, clause, defaultWt, false,
                                 idx, false, false, false, 0.0);
    if (app)
    {
      mln->setFormulaNumPreds(oss.str(), 1);
      mln->setFormulaIsHard(oss.str(), false);
      mln->setFormulaPriorMean(oss.str(), defaultWt);
    }
  }
}


void zzappendFormulaClausesToMLN(const ListObj* const & formula,
                                 const string& formulaStr,
                                 const int& numPreds,
                                 const double* const & wt,
                                 const double& defaultWt,
                                 const Domain* const & domain,
                                 MLN* const & mln,
                                 const ZZVarNameToIdMap& varNameToIdMap,
                                 const StringToIntMap& plusVarMap,
                                 const int& numAsterisk,
                                 const bool& hasFullStop,
                                 const bool& readHardClauseWts,
                                 const bool& mustHaveWtOrFullStop,
                                 const bool& isIndivisible,
                                 const bool& isHybrid,
                                 const ListObj* const & contPred,
                                 const double mean,
                                 const bool& hasWeightFullStop,
                                 const double* const & util,
                                 Array<int>& hardClauseIdxs,
                                 Array<string>& hardFormulas,
                                 Clause*& flippedClause,
                                 const Domain* const & domain0)
{
  //cout << "orig formula = " << endl << "\t: " << formulaStr << endl;
  //cout << "formula      = " << endl << "\t: " << *formula << endl;

  VarTypeMap* vtMap = zzcreateVarTypeMap(varNameToIdMap);
  Array<ListObj*> formulas;
  Array<string> formulaStrs;
  zzgroundPlusVar(formula, formulaStr, plusVarMap, formulas, formulaStrs,
                  domain, domain0);
  delete formula;

  for (int f = 0; f < formulas.size(); f++)
  {
    //cout<<"formula (after gnding '+')= "<<endl<<"\t: "<< *(formulas[f])<<endl;

    Array<ListObj*> formulas2;
    Array<string> formulaStrs2;
    zzpermuteAsteriskedPreds(numAsterisk, formulas[f], formulaStrs[f],
                             formulas2, formulaStrs2);
    delete formulas[f];

    for (int g = 0; g < formulas2.size(); g++)
    {
      string formStr = formulaStrs2[g];

      //cout << "formula (after *) " << endl << "\t: " << *(formulas2[g])<<endl;
      ListObj* vars = new ListObj;
      bool hasExist = false;
      ListObj* cnf = ListObj::toCNF(formulas2[g], vars, domain, vtMap, hasExist);
      delete formulas2[g];
      //cout << "cnf = " << endl << "\t: " << *cnf << endl;

      cnf->cleanUpVars();
      //cout << "cnf (after cleanUp) = " << endl << "\t: " << *cnf << endl;

      //commented out: not likely for there to be redundant clauses and is slow
      //replaced with removeRedundantPredicates()
      //cnf->removeRedundantClauses();

      cnf->removeRedundantPredicates();
      //cout << "cnf (removed redundant preds) = " <<endl<<"\t: "<<*cnf<<endl;

      Array<Clause*> clauses;
      zzcreateClauses(cnf, clauses, flippedClause, isIndivisible);

        // Output message of cnf size only if more than one
      if (clauses.size() > 1)
        cout << "\tCNF has  " << clauses.size() << " clauses" << endl;

      delete cnf; delete vars;

      double perClauseWt = 0;
      double formulaWt = 0;
      bool setHardWtLater = false;

      if (hasFullStop) // if this is a hard clause/formula
      {
        assert(wt == NULL);
        if (readHardClauseWts)
        {
          if (wt)
          { perClauseWt = (*wt)/clauses.size(); formulaWt = (*wt); }
          else
          {   //set weight later to twice of max soft clause wt
            perClauseWt = 1; formulaWt = 1;
            hardFormulas.append(formStr);
            setHardWtLater = true;
          }
        }
        else
        {   //set later to twice of max soft clause wt
          perClauseWt = 1; formulaWt = 1;
          hardFormulas.append(formStr);
          setHardWtLater = true;
        }
      }
      else
      if (wt)
      { perClauseWt = (*wt)/clauses.size(); formulaWt = *wt; }
      else
      {
          // It's ok to have no weight if there is a utility
        if (mustHaveWtOrFullStop && !util)
          zzerr("a weight or full stop must be specified for:\n%s",
                formStr.c_str());
        perClauseWt = defaultWt/clauses.size();
        formulaWt = defaultWt;
      }


      for (int i = 0; i < clauses.size(); i++)
      {
        ////// need a flag zzflipWtOfFlippedClause to indicate whether we should
        ////// flip the sign of the wt of a flipped clause.
        ////// During weight learning, we need not flip the sign because the
        ////// specified wt is a prior mean. During inference, we should flip
        ////// the sign because it's a real wt. This flag would have to
        ////// be passed in via runYYParser
        double clauseWt = perClauseWt;
        double clauseUtil = 0.0;
        if (util) clauseUtil = *util;
        bool conjunction = false;
        if (flippedClause && flippedClause == clauses[i])
        {
          if (zzflipWtsOfFlippedClause)
            clauseWt = -clauseWt;
          else
            conjunction = true;
        }

        int prevIdx;
        bool ok = false;

        if (isHybrid)
        {
          Predicate* pred = zzcreatePred(contPred);
          ok = mln->appendHybridClause(formStr, clauses[i], clauseWt, prevIdx,
                                       pred, mean);
        }
        else
        {
          ok = mln->appendClause(formStr, hasExist, clauses[i],
                                 clauseWt, hasFullStop, prevIdx,
                                 isIndivisible, hasWeightFullStop, conjunction,
                                 clauseUtil);
        }

        if (!ok)
        {
          cout << "\tsame clause (derived from another formula) has been added "
               << "to MLN:\n\t";
          const Clause* cl;
          if (isHybrid)
          {
            cout << formStr << endl;
          }
          else
          {
            cl = mln->getClause(prevIdx);
            cl->printWithoutWt(cout,domain); cout << endl;
          }
          //cout << " derived from current formula:\n\t" << formStr << endl;
        }

        if (setHardWtLater) hardClauseIdxs.append(prevIdx);
      }

      if (!isHybrid)
      {
        mln->setFormulaNumPreds(formStr, numPreds);
        mln->setFormulaPriorMean(formStr, formulaWt);
        mln->setFormulaWt(formStr, formulaWt);
        mln->setFormulaIsHard(formStr, hasFullStop);
      }

    } //for (int g = 0; g < formulas2.size(); g++)
  }//for (int f = 0; f < formulas.size(); f++)
  delete vtMap;
}


void zzappendFormulasToMLN(Array<ZZFormulaInfo*>& formulaInfos,
                           MLN* const & mln, const Domain* const & domain0)
{
  cout << "converting to CNF:" << endl;

  Array<int> hardClauseIdxs;
  Array<string> hardFormulas;
  Clause* flippedClause = NULL;

  for (int i = 0; i < formulaInfos.size(); i++)
  {
    double startSec = zztimer.time();
    ZZFormulaInfo* epfi = formulaInfos[i];
    cout << "formula " << i << ": " << epfi->formulaStr << endl;
    assert(mln == epfi->mln);
    zzappendFormulaClausesToMLN(epfi->formula, epfi->formulaStr, epfi->numPreds,
                                epfi->wt, epfi->defaultWt, epfi->domain,
                                epfi->mln, epfi->varNameToIdMap,
                                epfi->plusVarMap, epfi->numAsterisk,
                                epfi->hasFullStop,
                                epfi->readHardClauseWts,
                                epfi->mustHaveWtOrFullStop,
                                epfi->isIndivisible, epfi->isHybrid,
                                epfi->contPred, epfi->mean,
                                epfi->hasWeightFullStop, epfi->util,
                                hardClauseIdxs, hardFormulas,
                                flippedClause, domain0);
    delete epfi;
    cout<<"CNF conversion took ";Timer::printTime(cout,zztimer.time()-startSec);
    cout<<endl;
  }
  formulaInfos.clear();

  //set the weights of hard clauses
  double maxSoftWt = mln->getMaxAbsSoftWt();
  if (maxSoftWt == 0) maxSoftWt = 1;

  double hardWt = (HARD_WEIGHT==DBL_MIN) ?  HARD_WEIGHT_MULTIPLIER * maxSoftWt
                                          : HARD_WEIGHT;

  for (int i = 0; i < hardClauseIdxs.size(); i++)
  {
    ////// need a flag zzflipWtOfFlippedClause to indicate whether we should
    ////// flip the sign of the wt of a flipped clause.
    ////// during weight learning, we need not flip the sign because the
    ////// specified wt is a prior mean. During inference, we should flip
    ////// the sign because it's a real wt. This flag would have to
    ////// be passed in via runYYParser
    double hhardWt = hardWt;
    /*
    if (flippedClause &&
        //flippedClause->same( (Clause*)mln->getClause(hardClauseIdxs[i]) )
        flippedClause == (Clause*)mln->getClause(hardClauseIdxs[i])
        && zzflipWtsOfFlippedClause)
      hhardWt = -hhardWt;
    */

      // Weight has been flipped when added to mln. So, if weight
      // is neg. and marked as hard, then need to flip hard weight
    if (zzflipWtsOfFlippedClause &&
        ((Clause*)mln->getClause(hardClauseIdxs[i]))->getWt() < 0)
      hhardWt = -hhardWt;

    ((Clause*)mln->getClause(hardClauseIdxs[i]))->setWt(hhardWt);

    // HP:
    if (hhardWt>0) ((Clause*)mln->getClause(hardClauseIdxs[i]))->setIsHardClause(true);
  }

  for (int i = 0; i < hardFormulas.size(); i++)
  {
    mln->setFormulaWt(hardFormulas[i], hardWt);
    mln->setFormulaPriorMean(hardFormulas[i], hardWt);
  }

}


void zzsigHandler(int signo)
{
  if (zznumErrors > 0) printf("Num of errors detected = %d\n", zznumErrors);
  if (zzisParsing)
    printf("UNRECOVERABLE ERROR in %s: line %d, col %d\n",
           rmTmpPostfix(zzinFileName).c_str(), zzline, zzcolumn);
  else
    printf("UNRECOVERABLE ERROR after parsing %s\n",
           rmTmpPostfix(zzinFileName).c_str());

  zzok = false;
  signal(signo,SIG_DFL);
}

/**
 * Compiles a C++ file containing linked-in functions into a shared object file.
 * The old version of the target file is removed, if it exists, then the C++
 * file is compiled. If the old target file can not be removed or if the C++
 * file can not be compiled then the program exits.
 *
 * @fileName absolute path to file to be compiled.
 */
void zzcompileFunctions(const char* fileName)
{
  ifstream infs;
  ofstream outfs;

  // First remove any old .so file
  char* removeso;
  removeso = (char *)malloc((strlen("rm -f ") +
  							strlen(ZZ_FUNCTION_SO_FILE) + 1)*sizeof(char));
  strcpy(removeso, "rm -f ");
  strcat(removeso, ZZ_FUNCTION_SO_FILE);
  system(removeso);

  // If .so file is still there, then exit
  infs.open(ZZ_FUNCTION_SO_FILE, ifstream::in);
  infs.close();
  if(!infs.fail())
  {
  	infs.clear(ios::failbit);
	cout << "Unable to remove " << ZZ_FUNCTION_SO_FILE << endl;
	exit(-1);
  }

  // Compile the file
  char* systemcall;
  systemcall = (char *)malloc((strlen("g++ -fPIC -shared -o ") +
  								strlen(ZZ_FUNCTION_SO_FILE) +
								strlen(" ") +
								strlen(fileName) + 1)*sizeof(char));
  strcpy(systemcall, "g++ -fPIC -shared -o ");
  strcat(systemcall, ZZ_FUNCTION_SO_FILE);
  strcat(systemcall, " ");
  strcat(systemcall, fileName);
  system(systemcall);

  // If .so file is not there, then exit
  infs.open(ZZ_FUNCTION_SO_FILE, ifstream::in);
  infs.close();
  if(infs.fail())
  {
  	infs.clear(ios::failbit);
	cout << "Could not compile function file " << fileName << endl;
	exit(-1);
  }
  return;
}


/**
 * Inserts one permutation of constants for a function to take as
 * arguments.
 *
 * @param domain the domain from which the constants are used
 *
 * @param funccall function call obtained from dlsym() (dynamic library)
 *
 * @param ftemplate function template present for the function in the
 * given domain
 *
 * @numTerms number of terms which the function takes
 *
 * @currentConstants counters for each term, telling us which constant is
 * currently being inserted
 *
 */
void zzinsertPermutationOfLinkedFunction(const Domain* const & domain,
                                         void* funccall,
                                         const FunctionTemplate* ftemplate,
                                         int numTerms,
                                         Array<int>* currentConstants)
{
  string retString;
  string arguments[numTerms];
  string argumentsAsNum[numTerms];

  // Find the arguments for the function according to currentConstants
  for (int i = 0; i < numTerms; i++)
  {
    const Array<int>* constantsByType =
      domain->getConstantsByType(ftemplate->getTermTypeAsInt(i));

    arguments[i] =
      domain->getConstantName((*constantsByType)[((*currentConstants)[i])]);
	// If constant is a number, then we have to cut it out of the string
    // C@Type@Number
    unsigned int at = arguments[i].rfind("@");
    if (at != string::npos)
      argumentsAsNum[i] = arguments[i].substr(at+1, arguments[i].length()-at-1);
    else argumentsAsNum[i] = arguments[i];
  }

  // Make the function call (max. 5 arguments)
  switch (numTerms)
  {
    case 0:
      retString = (*(string (*)())(funccall))();
      break;
    case 1:
      retString = (*(string (*)(string))(funccall))(argumentsAsNum[0]);
      break;
    case 2:
      retString = (*(string (*)(string, string))(funccall))
                    (argumentsAsNum[0], argumentsAsNum[1]);
      break;
    case 3:
      retString = (*(string (*)(string, string, string))(funccall))
                    (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2]);
      break;
    case 4:
      retString = (*(string (*)(string, string, string, string))(funccall))
                    (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2],
                     argumentsAsNum[3]);
      break;
    case 5:
      retString = (*(string (*)(string, string, string, string, string))
                    (funccall))
                    (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2],
                     argumentsAsNum[3], argumentsAsNum[4]);
      break;
    default:
      cout << "Linked-in functions can take max. 5 arguments\n" << endl;
      return;
  }

  // If a number is returned, then we have to make a constant out of it
  int i;
  istringstream iss(retString);
  char constName[1000];
  if (iss>>i) // We are dealing with an integer
    zzcreateIntConstant(constName, ftemplate->getRetTypeName(), i);
  else
    strcpy(constName, retString.c_str());

  // The return value has to be an existing constant of the return type
  int constantId = domain->getConstantId(constName);
  const Array<int>* returnConstants =
    domain->getConstantsByType(ftemplate->getRetTypeId());

  if (returnConstants->contains(constantId))
  {
      // Insert the function definition just created
      // Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
    char* predName;
    predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
                               strlen(ftemplate->getName()) + 1)*sizeof(char));
    strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
    strcat(predName, ftemplate->getName());
    zzcreatePred(zzpred, predName);
    zzpred->setTruthValue(TRUE);

      //Add return constant to predicate
    zzpredAppendConstant(zzpred, constantId, constName);
      //Add constant terms to predicate
    for (int i = 0; i < numTerms; i++)
    {
      const char* term = arguments[i].c_str();
      int constId = domain->getConstantId(term);
      zzpredAppendConstant(zzpred, constId, term);
    }

    zzcheckPredNumTerm(zzpred);
    int predId = zzpred->getId();

      // Insert mapping of grounding
    hash_map<int,PredicateHashArray*>::iterator it;
    if ((it=zzpredIdToGndPredMap.find(predId)) == zzpredIdToGndPredMap.end())
      zzpredIdToGndPredMap[predId] = new PredicateHashArray;

//cout << "Mapping " << endl;
//zzpred->printWithStrVar(cout, zzdomain);
//cout << " " << zzpred->getTruthValue() << endl;

    PredicateHashArray* pha = zzpredIdToGndPredMap[predId];
    if (pha->append(zzpred) < 0)
    {
      int a = pha->find(zzpred);
      zzassert(a >= 0, "expecting ground predicate to be found");
      string origTvStr = (*pha)[a]->getTruthValueAsStr();
      (*pha)[a]->setTruthValue(zzpred->getTruthValue());
      string newTvStr = (*pha)[a]->getTruthValueAsStr();

      if (zzwarnDuplicates)
      {
        ostringstream oss;
        oss << "Duplicate ground predicate "; zzpred->print(oss, zzdomain);
        oss << " found. ";
        if (origTvStr.compare(newTvStr) != 0)
          oss << "Changed its truthValue from " << origTvStr << " to "
              << newTvStr << endl;
        zzwarn(oss.str().c_str());
      }
  	  delete zzpred;
    }

    delete [] predName;
    zzpred = NULL;
  }
  //delete returnConstants;
}

/**
 * Inserts all permutations of constants for a function to take as
 * arguments.
 *
 * @param domain the domain from which the constants are used
 *
 * @param funccall function call obtained from dlsym() (dynamic library)
 *
 * @param ftemplate function template present for the function in the
 * given domain
 *
 * @numTerms number of terms which the function takes
 *
 * @currentTerm number of the current term
 *
 * @currentConstants counters for each term, telling us which constant is
 * currently being inserted
 *
 */
void zzinsertPermutationsOfLinkedFunction(const Domain* const & domain,
                                          void* funccall,
                                          const FunctionTemplate* ftemplate,
                                          int numTerms, int currentTerm,
                                          Array<int>* currentConstants)
{
  const Array<int>* constants =
    domain->getConstantsByType(ftemplate->getTermTypeAsInt(currentTerm));

    // Base case: at the last term
  if (currentTerm == numTerms - 1)
  {
    for (int i = 0; i < constants->size(); i++)
    {
      (*currentConstants)[currentTerm] = i;
      zzinsertPermutationOfLinkedFunction(domain, funccall, ftemplate, numTerms,
                                          currentConstants);
    }
    return;
  }

    // Not yet at last term
  zzinsertPermutationsOfLinkedFunction(domain, funccall, ftemplate, numTerms,
                                       currentTerm + 1, currentConstants);

  if (++(*currentConstants)[currentTerm] < constants->size())
    zzinsertPermutationsOfLinkedFunction(domain, funccall, ftemplate, numTerms,
                                         currentTerm, currentConstants);

  (*currentConstants)[currentTerm] = 0;
  return;
}

/**
 * Generates all valid groundings for a linked-in function.
 *
 * @param domain the domain from which the function names and constants
 * are used
 *
 * @param funcname name of function for which the groundings are
 * being produced
 *
 * @param handle handle obtained from dlopen() on a file name
 *
 */
void zzgenerateGroundingsFromLinkedFunction(const Domain* const & domain,
										    const char* funcname,
										    void* handle)
{
  char* error;
  void* funccall;

    // Obtain functioncall from dynamic library
  dlerror();    // Clear any existing error
  funccall = dlsym(handle, funcname);
  if ((error = dlerror()) != NULL)
  {
    printf("Error while evaluating function %s\n", funcname);
    fprintf (stderr, "dlerror: %s\n", error);
    return;
  }

    // Find number of terms for function
  const FunctionTemplate* ftemplate = domain->getFunctionTemplate(funcname);
  int numTerms = ftemplate->getNumTerms();

    // Insert all possible permutations of constants
  const Array<int>* termTypes = ftemplate->getTermTypesAsInt();
  zzassert(numTerms == termTypes->size(),
           "Number of terms and term types in function don't match");
  Array<int>* currentConstants = new Array<int>;
  for (int i = 0; i < numTerms; i++) currentConstants->append(0);
  zzinsertPermutationsOfLinkedFunction(domain, funccall, ftemplate, numTerms, 0,
                                       currentConstants);

  return;
}

/**
 * Generates all valid groundings from all linked in functions based on
 * the constants present in a domain. Looks at each declared function in
 * the domain and if it is a linked-in function, then the groundings are
 * generated.
 *
 * @param domain The domain from which the function names and constants
 * are used
 *
 */
void zzgenerateGroundingsFromLinkedFunctions(const Domain* const & domain)
{
    // First check if a file with functions exists
  void *handle;
  char* openFileName;
  openFileName = (char *)malloc((strlen("./") +
                                 strlen(ZZ_FUNCTION_SO_FILE) + 1)*sizeof(char));
  strcpy(openFileName, "./");
  strcat(openFileName, ZZ_FUNCTION_SO_FILE);
  handle = dlopen(openFileName, RTLD_LAZY);
  if (!handle)
  {
      // Can not open file, so no linked-in functions
    printf("No file for linked-in functions found.\n");
    fprintf (stderr, "%s\n", dlerror());
    dlclose(handle);
    return;
  }

    // Look at each function
  const Array<const char*>* fnames = domain->getFunctionNames();
  for (int i = 0; i < fnames->size(); i++)
  {
      // If it is a linked-in function,
      // then generate groundings for each permutation of the given types
    if (!zzisInternalFunction((*fnames)[i]) &&
        zzisLinkedFunction((*fnames)[i], handle))
    {
      cout << "Found linked-in function: " << (*fnames)[i] << endl;
      zzgenerateGroundingsFromLinkedFunction(domain, (*fnames)[i], handle);
    }
  }
  dlclose(handle);
  return;
}


/**
 * Inserts one permutation of constants for a predicate to take as
 * arguments.
 *
 * @param domain the domain from which the constants are used
 *
 * @param funccall function call obtained from dlsym() (dynamic library)
 *
 * @param ptemplate predicate template present for the predicate in the
 * given domain
 *
 * @numTerms number of terms which the predicate takes
 *
 * @currentConstants counters for each term, telling us which constant is
 * currently being inserted
 *
 */
void zzinsertPermutationOfLinkedPredicate(const Domain* const & domain,
                                          void* funccall,
                                          const PredicateTemplate* ptemplate,
                                          int numTerms,
                                          Array<int>* currentConstants)
{
  bool retBool = false;
  string arguments[numTerms];
  string argumentsAsNum[numTerms];

    // Find the arguments for the predicate according to currentConstants
  for (int i = 0; i < numTerms; i++)
  {
    const Array<int>* constantsByType =
      domain->getConstantsByType(ptemplate->getTermTypeAsInt(i));

    arguments[i] =
      domain->getConstantName((*constantsByType)[((*currentConstants)[i])]);
      // If constant is a number, then we have to cut it out of the string
      // C@Type@Number
    unsigned int at = arguments[i].rfind("@");
    if (at != string::npos)
      argumentsAsNum[i] = arguments[i].substr(at+1, arguments[i].length()-at-1);
    else argumentsAsNum[i] = arguments[i];
  }

    // Make the function call (max. 5 arguments)
  switch (numTerms)
  {
    case 0:
      retBool = (*(bool (*)())(funccall))();
      break;
    case 1:
      retBool = (*(bool (*)(string))(funccall))(argumentsAsNum[0]);
      break;
    case 2:
      retBool = (*(bool (*)(string, string))(funccall))
                    (argumentsAsNum[0], argumentsAsNum[1]);
      break;
    case 3:
      retBool = (*(bool (*)(string, string, string))(funccall))
                    (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2]);
      break;
    case 4:
      retBool = (*(bool (*)(string, string, string, string))(funccall))
                    (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2],
                     argumentsAsNum[3]);
      break;
    case 5:
      retBool = (*(bool (*)(string, string, string, string, string))(funccall))
                    (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2],
                     argumentsAsNum[3], argumentsAsNum[4]);
      break;
    default:
      cout << "Linked-in predicates can take max. 5 arguments\n" << endl;
      return;
  }

    // Insert the predicate definition just created
  const char* predName;
  predName = ptemplate->getName();
  //for (int i = 0; i < currentConstants->size(); i++)
    //printf("%d ", (*currentConstants)[i]);
  zzcreatePred(zzpred, predName);
  if (retBool) zzpred->setTruthValue(TRUE);
  else zzpred->setTruthValue(FALSE);

    // Add constant terms to predicate
  for (int i = 0; i < numTerms; i++)
  {
    const char* term = arguments[i].c_str();
    int constId = domain->getConstantId(term);
    zzpredAppendConstant(zzpred, constId, term);
  }

  zzcheckPredNumTerm(zzpred);
  int predId = zzpred->getId();

    // Insert mapping of grounding
  hash_map<int,PredicateHashArray*>::iterator it;
  if ((it=zzpredIdToGndPredMap.find(predId)) == zzpredIdToGndPredMap.end())
   	zzpredIdToGndPredMap[predId] = new PredicateHashArray;

//cout << "Mapping " << endl;
//zzpred->printWithStrVar(cout, zzdomain);
//cout << " " << zzpred->getTruthValue() << endl;

  PredicateHashArray* pha = zzpredIdToGndPredMap[predId];
  if (pha->append(zzpred) < 0)
  {
    int a = pha->find(zzpred);
    zzassert(a >= 0, "expecting ground predicate to be found");
    string origTvStr = (*pha)[a]->getTruthValueAsStr();
    (*pha)[a]->setTruthValue(zzpred->getTruthValue());
    string newTvStr = (*pha)[a]->getTruthValueAsStr();

    if (zzwarnDuplicates)
    {
      ostringstream oss;
      oss << "Duplicate ground predicate "; zzpred->print(oss, zzdomain);
      oss << " found. ";
      if (origTvStr.compare(newTvStr) != 0)
        oss << "Changed its truthValue from " << origTvStr << " to " << newTvStr
            << endl;
      zzwarn(oss.str().c_str());
    }
    delete zzpred;
  }
  zzpred = NULL;
}

/**
 * Inserts all permutations of constants for a predicate to take as
 * arguments.
 *
 * @param domain the domain from which the constants are used
 *
 * @param funccall function call obtained from dlsym() (dynamic library)
 *
 * @param ptemplate predicate template present for the predicate in the
 * given domain
 *
 * @numTerms number of terms which the predicate takes
 *
 * @currentTerm number of the current term
 *
 * @currentConstants counters for each term, telling us which constant is
 * currently being inserted
 *
 */
void zzinsertPermutationsOfLinkedPredicate(const Domain* const & domain,
                                           void* funccall,
                                           const PredicateTemplate* ptemplate,
                                           int numTerms, int currentTerm,
                                           Array<int>* currentConstants)
{
  const Array<int>* constants =
    domain->getConstantsByType(ptemplate->getTermTypeAsInt(currentTerm));

    // Base case: at the last term
  if (currentTerm == numTerms - 1)
  {
    for (int i = 0; i < constants->size(); i++)
    {
      (*currentConstants)[currentTerm] = i;
      zzinsertPermutationOfLinkedPredicate(domain, funccall, ptemplate,
                                           numTerms, currentConstants);
    }
    return;
  }

    // Not yet at last term
  zzinsertPermutationsOfLinkedPredicate(domain, funccall, ptemplate, numTerms,
                                        currentTerm + 1, currentConstants);

  if (++(*currentConstants)[currentTerm] < constants->size())
    zzinsertPermutationsOfLinkedPredicate(domain, funccall, ptemplate, numTerms,
                                          currentTerm, currentConstants);

  (*currentConstants)[currentTerm] = 0;
  return;
}

/**
 * Generates all valid groundings for a linked-in predicate.
 *
 * @param domain the domain from which the predicate names and constants
 * are used
 *
 * @param predicatename name of predicate for which the groundings are
 * being produced
 *
 * @param handle handle obtained from dlopen() on a file name
 *
 */
void zzgenerateGroundingsFromLinkedPredicate(const Domain* const & domain,
										     const char* predname,
										     void* handle)
{
  char* error;
  void* funccall;

    // Obtain functioncall from dynamic library
  dlerror();    // Clear any existing error
  funccall = dlsym(handle, predname);
  if ((error = dlerror()) != NULL)
  {
    printf("Error while evaluating predicate %s\n", predname);
    fprintf (stderr, "dlerror: %s\n", error);
    return;
  }

    // Find number of terms for predicate
  const PredicateTemplate* ptemplate = domain->getPredicateTemplate(predname);
  int numTerms = ptemplate->getNumTerms();

    // Insert all possible permutations of constants
  const Array<int>* termTypes = ptemplate->getTermTypesAsInt();
  zzassert(numTerms == termTypes->size(),
           "Number of terms and term types in function don't match");
  Array<int>* currentConstants = new Array<int>;
  for (int i = 0; i < numTerms; i++) currentConstants->append(0);
  zzinsertPermutationsOfLinkedPredicate(domain, funccall, ptemplate, numTerms,
                                        0, currentConstants);

  return;
}

/**
 * Generates all valid groundings from all linked in predicates based on
 * the constants present in a domain. Looks at each declared predicate in
 * the domain and if it is a linked-in predicate, then the groundings are
 * generated.
 *
 * @param domain The domain from which the predicate names and constants
 * are used
 *
 */
void zzgenerateGroundingsFromLinkedPredicates(const Domain* const & domain)
{
    // First check if a file with predicates exists
  void *handle;
  char* openFileName;
  openFileName = (char *)malloc((strlen("./") +
                                 strlen(ZZ_FUNCTION_SO_FILE) + 1)*sizeof(char));
  strcpy(openFileName, "./");
  strcat(openFileName, ZZ_FUNCTION_SO_FILE);
  handle = dlopen(openFileName, RTLD_LAZY);
  if (!handle)
  {
      // Can not open file, so no linked-in predicates
    printf("No file for linked-in predicates found.\n");
    fprintf (stderr, "%s\n", dlerror());
    dlclose(handle);
    return;
  }

    // Look at each predicate
  const Array<const char*>* pnames = domain->getPredicateNames();
  for (int i = 0; i < pnames->size(); i++)
  {
      // If it is a linked-in predicate,
      // then generate groundings for each permutation of the given types
    if (!zzisInternalPredicate((*pnames)[i]) &&
        zzisLinkedPredicate((*pnames)[i], handle))
    {
      cout << "Found linked-in predicate: " << (*pnames)[i] << endl;
      zzgenerateGroundingsFromLinkedPredicate(domain, (*pnames)[i], handle);
    }
  }
  dlclose(handle);
  return;
}

/**
 * Declares all internally implemented predicates and functions
 * (see zzinternalPredicates and zzinternalFunctions).
 * (no longer used, internals are declared on-the-fly)
 */
/*
void zzdeclareInternalPredicatesAndFunctions()
{
  // Predicates
  for (int i = 0; i < zzinternalPredicates.size(); i++)
  {
  	const char* predName = zzinternalPredicates[i][0];
	  //predicate has not been declared a function
  	zzassert(zzdomain->getFunctionId(predName) < 0,
    	       "not expecting pred name to be declared as a function name");
  	zzassert(zzpredTemplate==NULL,"expecting zzpredTemplate==NULL");
  	zzpredTemplate = new PredicateTemplate();
  	zzpredTemplate->setName(predName);

  	// Add types
  	for (int j = 1; j < zzinternalPredicates[i].size(); j++)
  	{
  	  int id;
  	  const char* ttype = zzinternalPredicates[i][j];
  	  if (!zzdomain->isType(ttype))
  	  {
		id = zzaddTypeToDomain(zzdomain, ttype);
  		zzassert(id >= 0, "expecting var id >= 0");
  	  }
  	  zzaddType(ttype, zzpredTemplate, NULL, false, zzdomain);
	  //delete [] ttype;
  	}

  	// Add template to domain
  	zzassert(zzpredTemplate, "not expecting zzpredTemplate==NULL");
	int id = zzdomain->addPredicateTemplate(zzpredTemplate);
  	zzassert(id >= 0, "expecting pred template id >= 0");
  	zzpredTemplate->setId(id);
  	zzpredTemplate = NULL;
  }


  // Functions
  for (int i = 0; i < zzinternalFunctions.size(); i++)
  {
	zzassert(zzfuncTemplate==NULL, "expecting zzfuncTemplate==NULL");
	zzfuncTemplate = new FunctionTemplate();

	// We are creating a new predicate as well
  	zzassert(zzpredTemplate==NULL,"expecting zzpredTemplate==NULL");
  	zzpredTemplate = new PredicateTemplate();

  	const char* funcName = zzinternalFunctions[i][0];

	zzassert(zzdomain->getPredicateId(funcName) < 0,
    	     "not expecting func name to be declared as pred name");
  	zzassert(zzfuncTemplate,"expecting zzfuncTemplate!=NULL");
	zzfuncTemplate->setName(funcName);

	// Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
	char* predName;
	predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
  							strlen(funcName) + 1)*sizeof(char));
	strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
	strcat(predName, funcName);

	// Check that predicate has not been declared a function
	zzassert(zzdomain->getFunctionId(predName) < 0,
  		     "not expecting pred name to be declared as a function name");
  	zzassert(zzpredTemplate,"expecting zzpredTemplate!=NULL");
 	zzpredTemplate->setName(predName);
	delete [] predName;

  	// Add return type
  	const char* retTypeName = zzinternalFunctions[i][1];

	if (!zzdomain->isType(retTypeName))
  	{
   	  int id = zzaddTypeToDomain(zzdomain, retTypeName);
      zzassert(id >= 0, "expecting retTypeName's id >= 0");
  	}

	zzfuncTemplate->setRetTypeName(retTypeName,zzdomain);
  	// We are creating a new predicate as well
	zzaddType(retTypeName, zzpredTemplate, NULL, false, zzdomain);

  	// Add types
  	for (int j = 2; j < zzinternalFunctions[i].size(); j++)
  	{
  	  int id;
  	  const char* ttype = zzinternalFunctions[i][j];
  	  if (!zzdomain->isType(ttype))
  	  {
		id = zzaddTypeToDomain(zzdomain, ttype);
  		zzassert(id >= 0, "expecting var id >= 0");
  	  }
  	  zzaddType(ttype, zzpredTemplate, NULL, false, zzdomain);
	  // Add the type to the function too
	  zzaddType(ttype, NULL, zzfuncTemplate, false, zzdomain);
  	}

  // Add templates to domain
  zzassert(zzfuncTemplate, "expecting zzfuncTemplate != NULL");
  int id = zzdomain->addFunctionTemplate(zzfuncTemplate);
  zzassert(id >= 0, "expecting function template's id >= 0");
  zzfuncTemplate->setId(id);
  zzfuncTemplate = NULL;

  zzassert(zzpredTemplate, "not expecting zzpredTemplate==NULL");
  int predId = zzdomain->addPredicateTemplate(zzpredTemplate);
  zzassert(predId >= 0, "expecting pred template id >= 0");
  zzpredTemplate->setId(predId);
  zzpredTemplate = NULL;
  }

  return;
}
*/

/**
 * Inserts one permutation of constants for a predicate to take as
 * arguments. If a new internal predicate is added, then it has to be
 * registered here.
 *
 * @param index index of the internal predicate
 *
 * @param ptemplate predicate template present for the predicate in the
 * given domain
 *
 * @numTerms number of terms which the predicate takes
 *
 * @currentConstants counters for each term, telling us which constant is
 * currently being inserted
 */
void zzinsertPermutationOfInternalPredicate(int index,
                                      const PredicateTemplate* const& ptemplate,
                                            int numTerms,
                                            Array<int>* currentConstants)
{
  bool retBool = false;
  string arguments[numTerms];
  string argumentsAsNum[numTerms];

    // Find the arguments for the predicate according to currentConstants
  for (int i = 0; i < numTerms; i++)
  {
    const Array<int>* constantsByType =
      zzdomain->getConstantsByType(ptemplate->getTermTypeAsInt(i));

    arguments[i] =
      zzdomain->getConstantName((*constantsByType)[((*currentConstants)[i])]);
      // If constant is a number, then we have to cut it out of the string
      // C@Type@Number
    unsigned int at = arguments[i].rfind("@");
    if (at != string::npos)
      argumentsAsNum[i] = arguments[i].substr(at+1, arguments[i].length()-at-1);
    else
    {
      argumentsAsNum[i] = arguments[i];
        // Remove " from constants
      string::size_type loc = argumentsAsNum[i].find("\"", 0);
      while (loc != string::npos)
      {
        argumentsAsNum[i].erase(loc, 1);
        loc = argumentsAsNum[i].find("\"", 0);
      }
    }
  }

    // Make the function call
  int a, b;
  switch(index)
  {
    case 0:
      Internals::stringToInt(argumentsAsNum[0], a);
      Internals::stringToInt(argumentsAsNum[1], b);
      retBool = Internals::greaterThan(a, b);
      break;
    case 1:
      Internals::stringToInt(argumentsAsNum[0], a);
      Internals::stringToInt(argumentsAsNum[1], b);
      retBool = Internals::lessThan(a, b);
      break;
    case 2:
      Internals::stringToInt(argumentsAsNum[0], a);
      Internals::stringToInt(argumentsAsNum[1], b);
      retBool = Internals::greaterThanEq(a, b);
      break;
    case 3:
      Internals::stringToInt(argumentsAsNum[0], a);
      Internals::stringToInt(argumentsAsNum[1], b);
      retBool = Internals::lessThanEq(a, b);
      break;
    case 4:
      retBool = Internals::substr(argumentsAsNum[0], argumentsAsNum[1]);
      break;
  }

    // Insert the predicate definition just created
  const char* predName;
  predName = ptemplate->getName();
  zzcreatePred(zzpred, predName);
  if (retBool) zzpred->setTruthValue(TRUE);
  else zzpred->setTruthValue(FALSE);

    // Add constant terms to predicate
  for (int i = 0; i < numTerms; i++)
  {
    const char* term = arguments[i].c_str();
    int constId = zzdomain->getConstantId(term);
    zzpredAppendConstant(zzpred, constId, term);
  }

  zzcheckPredNumTerm(zzpred);
  int predId = zzpred->getId();

    // Insert mapping of grounding
  hash_map<int,PredicateHashArray*>::iterator it;
  if ((it=zzpredIdToGndPredMap.find(predId)) == zzpredIdToGndPredMap.end())
    zzpredIdToGndPredMap[predId] = new PredicateHashArray;

//cout << "Mapping " << endl;
//zzpred->printWithStrVar(cout, zzdomain);
//cout << " " << zzpred->getTruthValue() << endl;

  PredicateHashArray* pha = zzpredIdToGndPredMap[predId];
  if (pha->append(zzpred) < 0)
  {
    int a = pha->find(zzpred);
    zzassert(a >= 0, "expecting ground predicate to be found");
    string origTvStr = (*pha)[a]->getTruthValueAsStr();
    (*pha)[a]->setTruthValue(zzpred->getTruthValue());
    string newTvStr = (*pha)[a]->getTruthValueAsStr();

    if (zzwarnDuplicates)
    {
      ostringstream oss;
      oss << "Duplicate ground predicate "; zzpred->print(oss, zzdomain);
      oss << " found. ";
      if (origTvStr.compare(newTvStr) != 0)
        oss << "Changed its truthValue from " << origTvStr << " to " << newTvStr
            << endl;
      zzwarn(oss.str().c_str());
    }
    delete zzpred;
  }

  zzpred = NULL;
}

/**
 * Inserts one permutation of constants for a function to take as
 * arguments. If a new internal function is added, then it has to
 * be registered here.
 *
 * @param index index of the internal function
 *
 * @param ftemplate function template present for the function in the
 * given domain
 *
 * @numTerms number of terms which the function takes
 *
 * @currentConstants counters for each term, telling us which constant is
 * currently being inserted
 *
 */
void zzinsertPermutationOfInternalFunction(int index,
                                           const FunctionTemplate* ftemplate,
                                           int numTerms,
                                           Array<int>* currentConstants)
{
  char constName[1000];
  string arguments[numTerms];
  string argumentsAsNum[numTerms];

    // Find the arguments for the predicate according to currentConstants
  for (int i = 0; i < numTerms; i++)
  {
    const Array<int>* constantsByType =
      zzdomain->getConstantsByType(ftemplate->getTermTypeAsInt(i));

    arguments[i] =
      zzdomain->getConstantName((*constantsByType)[((*currentConstants)[i])]);
      // If constant is a number, then we have to cut it out of the string
      // C@Type@Number
    unsigned int at = arguments[i].rfind("@");
    if (at != string::npos)
      argumentsAsNum[i] = arguments[i].substr(at+1, arguments[i].length()-at-1);
    else argumentsAsNum[i] = arguments[i];
  }

    // Make the function call
  int a, b;
  switch(index)
  {
    case 0:
      Internals::stringToInt(argumentsAsNum[0], a);
      zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                          Internals::succ(a));
      break;
    case 1:
      Internals::stringToInt(argumentsAsNum[0], a);
      Internals::stringToInt(argumentsAsNum[1], b);
      zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                          Internals::plus(a, b));
      break;
    case 2:
      Internals::stringToInt(argumentsAsNum[0], a);
      Internals::stringToInt(argumentsAsNum[1], b);
      zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                          Internals::minus(a, b));
      break;
    case 3:
      Internals::stringToInt(argumentsAsNum[0], a);
      Internals::stringToInt(argumentsAsNum[1], b);
      zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                          Internals::times(a, b));
      break;
    case 4:
      Internals::stringToInt(argumentsAsNum[0], a);
      Internals::stringToInt(argumentsAsNum[1], b);
      zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                          Internals::dividedBy(a, b));
      break;
    case 5:
      Internals::stringToInt(argumentsAsNum[0], a);
      Internals::stringToInt(argumentsAsNum[1], b);
      zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                          Internals::mod(a, b));
      break;
    case 6:
      strcpy(constName,
             Internals::concat(argumentsAsNum[0], argumentsAsNum[1]).c_str());
  }

    // The return value has to be an existing constant of the return type
  int constantId = zzdomain->getConstantId(constName);
  const Array<int>* returnConstants =
    zzdomain->getConstantsByType(ftemplate->getRetTypeId());

  if (returnConstants->contains(constantId))
  {
      // Insert the function definition just created
      // Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
    char* predName;
    predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
                               strlen(ftemplate->getName()) + 1)*sizeof(char));
    strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
    strcat(predName, ftemplate->getName());
    zzcreatePred(zzpred, predName);
    zzpred->setTruthValue(TRUE);

      // Add return constant to predicate
    zzpredAppendConstant(zzpred, constantId, constName);
      // Add constant terms to predicate
    for (int i = 0; i < numTerms; i++)
    {
      const char* term = arguments[i].c_str();
      int constId = zzdomain->getConstantId(term);
      zzpredAppendConstant(zzpred, constId, term);
    }

    zzcheckPredNumTerm(zzpred);
    int predId = zzpred->getId();
      // Insert mapping of grounding
    hash_map<int,PredicateHashArray*>::iterator it;
    if ((it=zzpredIdToGndPredMap.find(predId)) == zzpredIdToGndPredMap.end())
      zzpredIdToGndPredMap[predId] = new PredicateHashArray;

//cout << "Mapping " << endl;
//zzpred->printWithStrVar(cout, zzdomain);
//cout << " " << zzpred->getTruthValue() << endl;

    PredicateHashArray* pha = zzpredIdToGndPredMap[predId];
    if (pha->append(zzpred) < 0)
    {
      int a = pha->find(zzpred);
      zzassert(a >= 0, "expecting ground predicate to be found");
      string origTvStr = (*pha)[a]->getTruthValueAsStr();
      (*pha)[a]->setTruthValue(zzpred->getTruthValue());
      string newTvStr = (*pha)[a]->getTruthValueAsStr();

      if (zzwarnDuplicates)
      {
        ostringstream oss;
        oss << "Duplicate ground predicate "; zzpred->print(oss, zzdomain);
        oss << " found. ";
        if (origTvStr.compare(newTvStr) != 0)
          oss << "Changed its truthValue from " << origTvStr << " to "
              << newTvStr << endl;
        zzwarn(oss.str().c_str());
      }
      delete zzpred;
    }

    free(predName);
    zzpred = NULL;
  }
  //delete returnConstants;
}

/**
 * Inserts all permutations of constants for a predicate to take as
 * arguments.
 *
 * @param index index of the internal predicate
 *
 * @param ptemplate predicate template present for the predicate in the
 * given domain
 *
 * @numTerms number of terms which the predicate takes
 *
 * @currentTerm number of the current term
 *
 * @currentConstants counters for each term, telling us which constant is
 * currently being inserted
 *
 */
void zzinsertPermutationsOfInternalPredicate(int index,
                                      const PredicateTemplate* const& ptemplate,
                                             int numTerms, int currentTerm,
                                             Array<int>* currentConstants)
{
  const Array<int>* constants =
    zzdomain->getConstantsByType(ptemplate->getTermTypeAsInt(currentTerm));

    // Base case: at the last term
  if (currentTerm == numTerms - 1)
  {
    for (int i = 0; i < constants->size(); i++)
    {
      (*currentConstants)[currentTerm] = i;
      zzinsertPermutationOfInternalPredicate(index, ptemplate, numTerms,
                                             currentConstants);
    }
    return;
  }

    // Not yet at last term
  zzinsertPermutationsOfInternalPredicate(index, ptemplate, numTerms,
                                          currentTerm + 1, currentConstants);

  if (++(*currentConstants)[currentTerm] < constants->size())
    zzinsertPermutationsOfInternalPredicate(index, ptemplate, numTerms,
                                            currentTerm, currentConstants);

  (*currentConstants)[currentTerm] = 0;
  return;
}


/**
 * Inserts all permutations of constants for a function to take as
 * arguments.
 *
 * @param index index of the internal function
 *
 * @param ftemplate function template present for the function in the
 * given domain
 *
 * @numTerms number of terms which the predicate takes
 *
 * @currentTerm number of the current term
 *
 * @currentConstants counters for each term, telling us which constant is
 * currently being inserted
 *
 */
void zzinsertPermutationsOfInternalFunction(int index,
                                       const FunctionTemplate* const& ftemplate,
                                       int numTerms, int currentTerm,
                                       Array<int>* currentConstants)
{
  const Array<int>* constants =
    zzdomain->getConstantsByType(ftemplate->getTermTypeAsInt(currentTerm));

    // Base case: at the last term
  if (currentTerm == numTerms - 1)
  {
    for (int i = 0; i < constants->size(); i++)
    {
      (*currentConstants)[currentTerm] = i;
      zzinsertPermutationOfInternalFunction(index, ftemplate, numTerms,
                                            currentConstants);
    }
    return;
  }

    // Not yet at last term
  zzinsertPermutationsOfInternalFunction(index, ftemplate, numTerms,
                                         currentTerm + 1, currentConstants);

  if (++(*currentConstants)[currentTerm] < constants->size())
    zzinsertPermutationsOfInternalFunction(index, ftemplate, numTerms,
                                           currentTerm, currentConstants);

  (*currentConstants)[currentTerm] = 0;
  return;
}

/**
 * Generates all valid groundings for an internal predicate.
 *
 * @param index Index of the internal predicate
 */
void zzgenerateGroundingsFromInternalPredicate(int index,
                                      const PredicateTemplate* const& ptemplate)
{
    // Find number of terms for predicate
  if (ptemplate != NULL)
  {
    int numTerms = ptemplate->getNumTerms();

      // Insert all possible permutations of constants
    const Array<int>* termTypes = ptemplate->getTermTypesAsInt();
    zzassert(numTerms == termTypes->size(),
             "Number of terms and term types in predicate don't match");
    Array<int>* currentConstants = new Array<int>;
    for (int i = 0; i < numTerms; i++) currentConstants->append(0);
    zzinsertPermutationsOfInternalPredicate(index, ptemplate, numTerms, 0,
                                            currentConstants);
    delete currentConstants;
  }
  return;
}

/**
 * Generates all valid groundings for an internal function.
 *
 * @param index Index of the internal function
 */
void zzgenerateGroundingsFromInternalFunction(int index,
                                       const FunctionTemplate* const& ftemplate)
{
  // Find number of terms for function
  if (ftemplate != NULL)
  {
    int numTerms = ftemplate->getNumTerms();

      // Insert all possible permutations of constants
    const Array<int>* termTypes = ftemplate->getTermTypesAsInt();
    zzassert(numTerms == termTypes->size(),
             "Number of terms and term types in predicate don't match");
    Array<int>* currentConstants = new Array<int>;
    for (int i = 0; i < numTerms; i++) currentConstants->append(0);
    zzinsertPermutationsOfInternalFunction(index, ftemplate, numTerms, 0,
                                           currentConstants);
    delete currentConstants;
  }
  return;
}

/**
 * Generates all valid groundings from internally implemented predicates and
 * functions  (see internalPredicates and internalFunctions).
 *
 * @param domain The domain from which the predicate / function names and
 * constants are used
 *
 */
void zzgenerateGroundingsFromInternalPredicatesAndFunctions()
{
    // Look at each predicate
  for (int i = 0; i < zzdomain->getNumPredicates(); i++)
  {
    const PredicateTemplate* ptemplate = zzdomain->getPredicateTemplate(i);
    if (ptemplate->isInternalPredicateTemplate())
    {
      cout << "Found internal predicate: " << ptemplate->getName() << endl;
      for (int j = 0; j < zzinternalPredicates.size(); j++)
      {
cout << "h1" << endl;
        if (strncmp(ptemplate->getName(), zzinternalPredicates[j][0],
                    strlen(zzinternalPredicates[j][0])) == 0)
        {
cout << "h2" << endl;
          zzgenerateGroundingsFromInternalPredicate(j, ptemplate);
cout << "h3" << endl;
          break;
        }
cout << "h4" << endl;
      }
    }
  }

    // Look at each function
  for (int i = 0; i < zzdomain->getNumFunctions(); i++)
  {
    const FunctionTemplate* ftemplate = zzdomain->getFunctionTemplate(i);
    if (ftemplate->isInternalFunctionTemplate())
    {
      cout << "Found internal function: " << ftemplate->getName() << endl;
      for (int j = 0; j < zzinternalFunctions.size(); j++)
      {
        if (strncmp(ftemplate->getName(), zzinternalFunctions[j][0],
                    strlen(zzinternalFunctions[j][0])) == 0)
        {
          zzgenerateGroundingsFromInternalFunction(j, ftemplate);
          break;
        }
      }
    }
  }

  return;
}

void zzcreateInternalPredTemplate(const string& predName,
                                  const char* const & ttype)
{
    // If already declared then return
  if (zzdomain->getPredicateId(predName.c_str()) >= 0) return;
  int index;
  string baseName = predName.substr(0, predName.find_last_of("_"));

  if ((index = zzfindInternalPredicate(baseName.c_str())) >= 0)
  {
    zzassert(zzdomain->getFunctionId(predName.c_str()) < 0,
             "not expecting pred name to be declared as a function name");
    PredicateTemplate* ptemplate = new PredicateTemplate();
    ptemplate->setName(predName.c_str());

      // Add types
    for (int j = 1; j < zzinternalPredicates[index].size(); j++)
    {
      int id;
      if (!zzdomain->isType(ttype))
      {
        id = zzaddTypeToDomain(zzdomain, ttype);
        zzassert(id >= 0, "expecting var id >= 0");
      }
      zzaddType(ttype, ptemplate, NULL, false, zzdomain);
    }

      // Add template to domain
    zzassert(ptemplate, "not expecting ptemplate==NULL");
    int id = zzdomain->addPredicateTemplate(ptemplate);
    zzassert(id >= 0, "expecting pred template id >= 0");
    ptemplate->setId(id);
  }
  else
    zzexit("Predicate %s is not an internal predicate.", predName.c_str());
}

void zzsetInternalPredTypeName(const char* const & predName, const int& typeId)
{
  const char * typeName = zzdomain->getTypeName(typeId);
  string intPredName =
    PredicateTemplate::createInternalPredTypeName(predName, typeName);
  zzcreateInternalPredTemplate(intPredName, typeName);
  const PredicateTemplate* t =
    zzdomain->getPredicateTemplate(intPredName.c_str());
  zzpred->setTemplate((PredicateTemplate*)t);
  zzassert(zzdomain->getPredicateTemplate(intPredName.c_str()) != NULL,
           "expect internal pred template != NULL");
  ListObj* predlo = zzpredFuncListObjs.top();
  predlo->replace(predName, intPredName.c_str());
}

void zzcreateInternalFuncTemplate(const string & funcName,
								  const Array<string>& typeNames)
{
    // If already declared then return
  if (zzdomain->getFunctionId(funcName.c_str()) >= 0) return;
  int index;
  string baseName = funcName.substr(0, funcName.find_first_of("_"));

  if ((index = zzfindInternalFunction(baseName.c_str())) >= 0)
  {
    zzassert(zzfuncTemplate==NULL, "expecting zzfuncTemplate==NULL");
    zzfuncTemplate = new FunctionTemplate();

      // We are creating a new predicate as well
    zzassert(zzpredTemplate==NULL,"expecting zzpredTemplate==NULL");
    zzpredTemplate = new PredicateTemplate();

    zzassert(zzdomain->getPredicateId(funcName.c_str()) < 0,
             "not expecting func name to be declared as pred name");
    zzassert(zzfuncTemplate,"expecting zzfuncTemplate!=NULL");
    zzfuncTemplate->setName(funcName.c_str());

      // Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
    char* predName;
    predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
                               strlen(funcName.c_str()) + 1)*sizeof(char));
    strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
    strcat(predName, funcName.c_str());

      // Check that predicate has not been declared a function
    zzassert(zzdomain->getFunctionId(predName) < 0,
             "not expecting pred name to be declared as a function name");
    zzassert(zzpredTemplate,"expecting zzpredTemplate!=NULL");
    zzpredTemplate->setName(predName);
    free(predName);

      // Add return type
    const char* retTypeName = typeNames[0].c_str();

    if (!zzdomain->isType(retTypeName))
    {
      int id = zzaddTypeToDomain(zzdomain, retTypeName);
      zzassert(id >= 0, "expecting retTypeName's id >= 0");
    }

    zzfuncTemplate->setRetTypeName(retTypeName, zzdomain);
      // We are creating a new predicate as well
    zzaddType(retTypeName, zzpredTemplate, NULL, false, zzdomain);

      // Add types
    for (int j = 1; j < typeNames.size(); j++)
    {
      int id;
      const char* ttype = typeNames[j].c_str();
      if (!zzdomain->isType(ttype))
      {
        id = zzaddTypeToDomain(zzdomain, ttype);
        zzassert(id >= 0, "expecting var id >= 0");
      }
      zzaddType(ttype, zzpredTemplate, NULL, false, zzdomain);
        // Add the type to the function too
      zzaddType(ttype, NULL, zzfuncTemplate, false, zzdomain);
    }

      // Add templates to domain
    zzassert(zzfuncTemplate, "expecting zzfuncTemplate != NULL");
    int id = zzdomain->addFunctionTemplate(zzfuncTemplate);
    zzassert(id >= 0, "expecting function template's id >= 0");
    zzfuncTemplate->setId(id);
    zzfuncTemplate = NULL;

    zzassert(zzpredTemplate, "not expecting zzpredTemplate==NULL");
    int predId = zzdomain->addPredicateTemplate(zzpredTemplate);
    zzassert(predId >= 0, "expecting pred template id >= 0");
    zzpredTemplate->setId(predId);
    zzpredTemplate = NULL;
  }
  else
    zzexit("Function %s is not an internal function.", funcName.c_str());
}

void zzsetInternalFuncTypeName(const char* const & funcName,
                               const Array<int>& typeIds)
{
  Array<string> typeNames(typeIds.size());
  for (int i = 0; i < typeIds.size(); i++)
    typeNames.append(zzdomain->getTypeName(typeIds[i]));
  string intFuncName =
    FunctionTemplate::createInternalFuncTypeName(funcName, typeNames);
  zzcreateInternalFuncTemplate(intFuncName, typeNames);

  const FunctionTemplate* t =
    zzdomain->getFunctionTemplate(intFuncName.c_str());
  zzfunc->setTemplate((FunctionTemplate*)t);
  zzassert(zzdomain->getFunctionTemplate(intFuncName.c_str()) != NULL,
           "expect internal func template != NULL");
  ListObj* funclo = zzpredFuncListObjs.top();
  funclo->replace(funcName, intFuncName.c_str());
}

const FunctionTemplate* zzgetGenericInternalFunctionTemplate(
                                                   const char* const & funcName)
{
  zzassert(FunctionTemplate::isInternalFunctionTemplateName(funcName),
           "expect internal function name");
  int index = zzfindInternalFunction(funcName);
  FunctionTemplate* funcTemplate = new FunctionTemplate();
  funcTemplate->setName(funcName);

    // Add return type
  funcTemplate->setRetTypeName(PredicateTemplate::ANY_TYPE_NAME, zzdomain);

    // Add types
  for (int j = 2; j < zzinternalFunctions[index].size(); j++)
  {
      // Add the type to the function
    zzaddType(PredicateTemplate::ANY_TYPE_NAME, NULL, funcTemplate, false,
              zzdomain);
  }
  return funcTemplate;
}

/**
 * Moves a term attached to the previous function / predicate to the current infix
 * function. If the parser encounters a term, it is first attached to the current
 * function / predicate. After encountering an infix function sign, the term has to
 * be transferred via this method.
 */
void moveTermToInfixFunction()
{
    // top in zzpredFuncListObjs must be infix function, second to top is pred /
    // func in which it is nested

  Term* term = NULL;
    // In a function
  if (!zzfuncStack.empty())
  {
    Function* prevFunc = zzfuncStack.top();
    term = prevFunc->removeLastTerm();
  }
    // Not in a function
  else
  {
    zzassert(zzpred, "expecting to be in a predicate");
    term = zzpred->removeLastTerm();
  }
  term->setParent(zzfunc, false);
  zzfunc->appendTerm(term);
  ListObj* lo = zzpredFuncListObjs.top();
  zzpredFuncListObjs.pop();
  lo->append((zzpredFuncListObjs.top())->removeLast());
  zzpredFuncListObjs.push(lo);
}

#endif
